Commit 2022-11-26 00:19 0f74a7a1

View on Github →

feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610) Add a bit of simple API to probability_measure and finite_measure.

Estimated changes

Modified src/measure_theory/measure/finite_measure.lean

added theorem measure_theory.finite_measure.apply_mono

added theorem measure_theory.finite_measure.eq_of_forall_apply_eq

added theorem measure_theory.finite_measure.eq_of_forall_measure_apply_eq

deleted theorem measure_theory.finite_measure.extensionality

added def measure_theory.finite_measure.restrict

added theorem measure_theory.finite_measure.restrict_apply

added theorem measure_theory.finite_measure.restrict_apply_measure

added theorem measure_theory.finite_measure.restrict_eq_zero_iff

added theorem measure_theory.finite_measure.restrict_mass

added theorem measure_theory.finite_measure.restrict_measure_eq

added theorem measure_theory.finite_measure.restrict_nonzero_iff

Modified src/measure_theory/measure/probability_measure.lean

added theorem measure_theory.probability_measure.apply_mono

added theorem measure_theory.probability_measure.coe_fn_univ_ne_zero

added theorem measure_theory.probability_measure.eq_of_forall_apply_eq

added theorem measure_theory.probability_measure.eq_of_forall_measure_apply_eq

deleted theorem measure_theory.probability_measure.extensionality

added theorem measure_theory.probability_measure.nonempty_of_probability_measure