Commit 2023-02-11 07:44 2e9fc2c9

View on Github →

feat: port MeasureTheory.MeasurableSpace (#2174)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/UnionLift.lean

added theorem Set.preimage_liftCover

added theorem Set.preimage_unionᵢLift

Modified Mathlib/Logic/Equiv/Set.lean

added def Equiv.Set.rangeInl

added theorem Equiv.Set.rangeInl_apply_inl

added def Equiv.Set.rangeInr

added theorem Equiv.Set.rangeInr_apply_inr

Created Mathlib/MeasureTheory/MeasurableSpace.lean

added theorem Filter.Eventually.exists_measurable_mem

added theorem Filter.Eventually.exists_measurable_mem_of_smallSets

added theorem Filter.principal_isMeasurablyGenerated_iff

added def IsCountablySpanning

added theorem Measurable.dite

added theorem Measurable.eval

added theorem Measurable.find

added theorem Measurable.fst

added theorem Measurable.indicator

added theorem Measurable.ite

added theorem Measurable.iterate

added theorem Measurable.measurable_of_countable_ne

added theorem Measurable.mono

added theorem Measurable.of_uncurry_left

added theorem Measurable.of_uncurry_right

added theorem Measurable.prod

added theorem Measurable.prod_map

added theorem Measurable.prod_mk

added theorem Measurable.snd

added theorem Measurable.subtype_coe

added theorem Measurable.subtype_map

added theorem Measurable.subtype_mk

added theorem Measurable.sumElim

added theorem Measurable.sumMap

added theorem MeasurableEmbedding.comp

added theorem MeasurableEmbedding.exists_measurable_extend

added theorem MeasurableEmbedding.id

added theorem MeasurableEmbedding.measurableSet_image

added theorem MeasurableEmbedding.measurableSet_preimage

added theorem MeasurableEmbedding.measurableSet_range

added theorem MeasurableEmbedding.measurable_comp_iff

added theorem MeasurableEmbedding.measurable_extend

added theorem MeasurableEmbedding.measurable_rangeSplitting

added theorem MeasurableEmbedding.of_measurable_inverse

added theorem MeasurableEmbedding.of_measurable_inverse_on_range

added theorem MeasurableEmbedding.subtype_coe

added structure MeasurableEmbedding

added def MeasurableEquiv.Set.prod

added def MeasurableEquiv.Set.rangeInl

added def MeasurableEquiv.Set.rangeInr

added def MeasurableEquiv.Set.singleton

added def MeasurableEquiv.Set.univ

added def MeasurableEquiv.Simps.apply

added def MeasurableEquiv.Simps.symm_apply

added theorem MeasurableEquiv.apply_symm_apply

added theorem MeasurableEquiv.coe_mk

added theorem MeasurableEquiv.coe_toEquiv

added theorem MeasurableEquiv.coe_toEquiv_symm

added theorem MeasurableEquiv.ext

added def MeasurableEquiv.finTwoArrow

added def MeasurableEquiv.funUnique

added theorem MeasurableEquiv.image_eq_preimage

added theorem MeasurableEquiv.measurableSet_image

added theorem MeasurableEquiv.measurableSet_preimage

added def MeasurableEquiv.ofUniqueOfUnique

added def MeasurableEquiv.piCongrRight

added def MeasurableEquiv.piEquivPiSubtypeProd

added def MeasurableEquiv.piFinSuccAboveEquiv

added def MeasurableEquiv.piFinTwo

added def MeasurableEquiv.piMeasurableEquivTprod

added def MeasurableEquiv.prodAssoc

added def MeasurableEquiv.prodComm

added def MeasurableEquiv.prodCongr

added def MeasurableEquiv.prodSumDistrib

added def MeasurableEquiv.refl

added theorem MeasurableEquiv.self_comp_symm

added theorem MeasurableEquiv.self_trans_symm

added def MeasurableEquiv.sumCompl

added def MeasurableEquiv.sumCongr

added def MeasurableEquiv.sumProdDistrib

added def MeasurableEquiv.sumProdSum

added def MeasurableEquiv.symm

added theorem MeasurableEquiv.symm_apply_apply

added theorem MeasurableEquiv.symm_comp_self

added theorem MeasurableEquiv.symm_mk

added theorem MeasurableEquiv.symm_preimage_preimage

added theorem MeasurableEquiv.symm_refl

added theorem MeasurableEquiv.symm_trans_self

added theorem MeasurableEquiv.toEquiv_injective

added def MeasurableEquiv.trans

added structure MeasurableEquiv

added theorem MeasurableSet.coe_bot

added theorem MeasurableSet.coe_compl

added theorem MeasurableSet.coe_empty

added theorem MeasurableSet.coe_insert

added theorem MeasurableSet.coe_inter

added theorem MeasurableSet.coe_sdiff

added theorem MeasurableSet.coe_singleton

added theorem MeasurableSet.coe_top

added theorem MeasurableSet.coe_union

added theorem MeasurableSet.exists_measurable_proj

added theorem MeasurableSet.image_inclusion'

added theorem MeasurableSet.image_inclusion

added theorem MeasurableSet.measurableSet_bliminf

added theorem MeasurableSet.measurableSet_blimsup

added theorem MeasurableSet.measurableSet_liminf

added theorem MeasurableSet.measurableSet_limsup

added theorem MeasurableSet.mem_coe

added theorem MeasurableSet.of_subtype_image

added theorem MeasurableSet.subtype_image

added theorem MeasurableSet.tProd

added theorem MeasurableSpace.comap_bot

added theorem MeasurableSpace.comap_comp

added theorem MeasurableSpace.comap_eq_generateFrom

added theorem MeasurableSpace.comap_generateFrom

added theorem MeasurableSpace.comap_id

added theorem MeasurableSpace.comap_le_iff_le_map

added theorem MeasurableSpace.comap_map_le

added theorem MeasurableSpace.comap_mono

added theorem MeasurableSpace.comap_sup

added theorem MeasurableSpace.comap_supᵢ

added theorem MeasurableSpace.gc_comap_map

added theorem MeasurableSpace.le_map_comap

added theorem MeasurableSpace.map_comp

added theorem MeasurableSpace.map_id

added theorem MeasurableSpace.map_inf

added theorem MeasurableSpace.map_infᵢ

added theorem MeasurableSpace.map_mono

added theorem MeasurableSpace.map_top

added theorem MeasurableSpace.monotone_comap

added theorem MeasurableSpace.monotone_map

added def MeasurableSpace.prod

added theorem QuotientGroup.measurable_coe

added theorem Subsingleton.measurable

added theorem comap_measurable

added theorem exists_measurable_piecewise

added theorem exists_measurable_piecewise_nat

added theorem isCountablySpanning_measurableSet

added theorem measurableSet_inl_image

added theorem measurableSet_inr_image

added theorem measurableSet_mulSupport

added theorem measurableSet_pi

added theorem measurableSet_pi_of_nonempty

added theorem measurableSet_preimage

added theorem measurableSet_prod

added theorem measurableSet_prod_of_nonempty

added theorem measurableSet_quotient

added theorem measurableSet_range_inl

added theorem measurableSet_range_inr

added theorem measurableSet_sum_iff

added theorem measurableSet_swap_iff

added theorem measurable_const'

added theorem measurable_find

added theorem measurable_findGreatest

added theorem measurable_find_greatest'

added theorem measurable_from_nat

added theorem measurable_from_prod_countable

added theorem measurable_from_quotient

added theorem measurable_from_top

added theorem measurable_fst

added theorem measurable_generateFrom

added theorem measurable_iff_comap_le

added theorem measurable_iff_le_map

added theorem measurable_inclusion

added theorem measurable_inl

added theorem measurable_inr

added theorem measurable_liftCover

added theorem measurable_of_countable

added theorem measurable_of_empty

added theorem measurable_of_empty_codomain

added theorem measurable_of_finite

added theorem measurable_of_measurable_on_compl_finite

added theorem measurable_of_measurable_on_compl_singleton

added theorem measurable_of_measurable_union_cover

added theorem measurable_of_restrict_of_restrict_compl

added theorem measurable_of_subsingleton_codomain

added theorem measurable_one

added theorem measurable_piEquivPiSubtypeProd

added theorem measurable_piEquivPiSubtypeProd_symm

added theorem measurable_pi_apply

added theorem measurable_pi_iff

added theorem measurable_pi_lambda

added theorem measurable_prod

added theorem measurable_prod_mk_left

added theorem measurable_prod_mk_right

added theorem measurable_quot_mk

added theorem measurable_quotient_mk''

added theorem measurable_quotient_mk'

added theorem measurable_snd

added theorem measurable_subtype_coe

added theorem measurable_sum

added theorem measurable_swap

added theorem measurable_swap_iff

added theorem measurable_tProd_elim'

added theorem measurable_tProd_elim

added theorem measurable_tProd_mk

added theorem measurable_to_countable

added theorem measurable_to_nat

added theorem measurable_unionᵢLift

added theorem measurable_unit

added theorem measurable_update