Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 13:28 6144710d

View on Github →

feat(measure_theory): add equivalence of measurable spaces

Estimated changes

Modified src/data/equiv/basic.lean

Modified src/data/set/basic.lean

added theorem set.prod_eq

added theorem set.range_coe_subtype

Modified src/measure_theory/borel_space.lean

added def ennreal.ennreal_equiv_nnreal

added def ennreal.ennreal_equiv_sum

added theorem ennreal.measurable_coe

added theorem ennreal.measurable_mul

added theorem ennreal.measurable_of_measurable_nnreal

added theorem ennreal.measurable_of_measurable_nnreal_nnreal

added def homemorph.to_measurable_equiv

modified def measure_theory.borel

added theorem measure_theory.borel_eq_subtype

added theorem measure_theory.borel_induced

added theorem measure_theory.measurable_finset_sum

modified theorem measure_theory.measurable_of_continuous

Modified src/measure_theory/measurable_space.lean

added theorem is_measurable_inl_image

added theorem is_measurable_inr_image

added theorem is_measurable_range_inl

added theorem is_measurable_range_inr

added theorem is_measurable_subtype_image

added theorem measurable_equiv.coe_eq

added def measurable_equiv.prod_comm

added def measurable_equiv.prod_congr

added def measurable_equiv.prod_sum_distrib

added def measurable_equiv.refl

added def measurable_equiv.set.prod

added def measurable_equiv.set.range_inl

added def measurable_equiv.set.range_inr

added def measurable_equiv.set.singleton

added def measurable_equiv.set.univ

added def measurable_equiv.sum_congr

added def measurable_equiv.sum_prod_distrib

added def measurable_equiv.sum_prod_sum

added def measurable_equiv.symm

added theorem measurable_equiv.symm_to_equiv

added def measurable_equiv.trans

added theorem measurable_equiv.trans_to_equiv

added structure measurable_equiv

added theorem measurable_inl

added theorem measurable_inr

added theorem measurable_of_measurable_union_cover

added theorem measurable_sum

added theorem measurable_sum_rec

added theorem measurable_unit