Commit 2022-07-15 23:14 dc7ab9e7

View on Github →

feat(measure_theory/measure/finite_measure_weak_convergence): Add some missing API lemmas. (#15205) Add API lemmas about extentionality of finite_measure and probability_measure, about 0 : finite_measure X, and about scalar multiplication on finite_measure.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.smul_to_nnreal

Modified src/measure_theory/measure/finite_measure_weak_convergence.lean

added theorem measure_theory.finite_measure.coe_fn_smul_apply

added theorem measure_theory.finite_measure.extensionality

added theorem measure_theory.finite_measure.mass_zero_iff

added theorem measure_theory.finite_measure.smul_test_against_nn_apply

added theorem measure_theory.finite_measure.zero.mass

added theorem measure_theory.finite_measure.zero.test_against_nn

added theorem measure_theory.finite_measure.zero.test_against_nn_apply

added theorem measure_theory.probability_measure.extensionality