Commit 2022-11-25 02:14 e4edb230

View on Github →

feat(measure_theory/group/fundamental_domain): add lemma measure_theory.is_fundamental_domain.mk_of_measure_univ_le (#17438) Also some supporting / related lemmas.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_nsmul

Modified src/data/set/pointwise/basic.lean

added theorem set.Union_inv_smul

added theorem set.Union_smul_eq_set_of_exists

Modified src/measure_theory/group/action.lean

modified theorem measure_theory.measure_preserving_smul

Modified src/measure_theory/group/fundamental_domain.lean

added theorem measure_theory.is_fundamental_domain.measure_eq_card_smul_of_smul_ae_eq_self

added theorem measure_theory.is_fundamental_domain.mk_of_measure_univ_le

Modified src/measure_theory/measure/ae_disjoint.lean

deleted theorem measure_theory.ae_disjoint.mono

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.ae_eq_univ_iff_measure_eq

added theorem measure_theory.ae_iff_measure_eq

added theorem measure_theory.ae_mem_iff_measure_eq

added theorem measure_theory.measure.pairwise_ae_disjoint_of_ae_disjoint_forall_ne_one

Modified src/measure_theory/measure/null_measurable.lean

added theorem measure_theory.measure_add_measure_compl₀