Commit 2025-04-03 10:57 89b96c22

View on Github →

chore: split MeasureTheory.MeasurableSpace.Basic (#23523)

  • MeasureTheory.MeasurableSpace.Constructions contains constructions of new measurable spaces/functions from old ones.
  • MeasureTheory.MeasurableSpace.MeasurablyGenerated contains the definition IsMeasurablyGenerated.
  • MeasureTheory.MeasurableSpace.Basic now does not import filters at all, as does .Constructions; this is enforced by an assert_not_exists Filter in the latter.

Estimated changes

deleted theorem ENat.measurable_iff
deleted theorem Measurable.and
deleted theorem Measurable.dite
deleted theorem Measurable.eq_mp
deleted theorem Measurable.eval
deleted theorem Measurable.exists
deleted theorem Measurable.find
deleted theorem Measurable.forall
deleted theorem Measurable.fst
deleted theorem Measurable.iff
deleted theorem Measurable.imp
deleted theorem Measurable.not
deleted theorem Measurable.or
deleted theorem Measurable.prod
deleted theorem Measurable.prodMap
deleted theorem Measurable.prodMk
deleted theorem Measurable.snd
deleted theorem Measurable.subtype_coe
deleted theorem Measurable.subtype_map
deleted theorem Measurable.subtype_mk
deleted theorem Measurable.sumElim
deleted theorem Measurable.sumMap
deleted theorem MeasurableSet.coe_bot
deleted theorem MeasurableSet.coe_compl
deleted theorem MeasurableSet.coe_empty
deleted theorem MeasurableSet.coe_himp
deleted theorem MeasurableSet.coe_insert
deleted theorem MeasurableSet.coe_inter
deleted theorem MeasurableSet.coe_sdiff
deleted theorem MeasurableSet.coe_top
deleted theorem MeasurableSet.coe_union
deleted theorem MeasurableSet.mem_coe
deleted theorem MeasurableSet.sep_finite
deleted theorem MeasurableSet.tProd
deleted theorem Set.measurable_restrict
deleted def measurableAtom
deleted theorem measurableAtom_subset
deleted theorem measurableSet_inl_image
deleted theorem measurableSet_inr_image
deleted theorem measurableSet_mem
deleted theorem measurableSet_not_mem
deleted theorem measurableSet_pi
deleted theorem measurableSet_preimage_up
deleted theorem measurableSet_prod
deleted theorem measurableSet_quotient
deleted theorem measurableSet_range_inl
deleted theorem measurableSet_range_inr
deleted theorem measurableSet_setOf
deleted theorem measurableSet_sum_iff
deleted theorem measurableSet_swap_iff
deleted theorem measurableSet_tendsto
deleted theorem measurable_compl
deleted theorem measurable_down
deleted theorem measurable_eq_mp
deleted theorem measurable_find
deleted theorem measurable_findGreatest'
deleted theorem measurable_findGreatest
deleted theorem measurable_from_nat
deleted theorem measurable_from_quotient
deleted theorem measurable_fst
deleted theorem measurable_iUnionLift
deleted theorem measurable_inclusion
deleted theorem measurable_inl
deleted theorem measurable_inr
deleted theorem measurable_liftCover
deleted theorem measurable_mem
deleted theorem measurable_piCongrLeft
deleted theorem measurable_pi_apply
deleted theorem measurable_pi_iff
deleted theorem measurable_pi_lambda
deleted theorem measurable_prod
deleted theorem measurable_prodMk_left
deleted theorem measurable_prodMk_right
deleted theorem measurable_quot_mk
deleted theorem measurable_quotient_mk''
deleted theorem measurable_quotient_mk'
deleted theorem measurable_set_iff
deleted theorem measurable_set_mem
deleted theorem measurable_set_not_mem
deleted theorem measurable_snd
deleted theorem measurable_subtype_coe
deleted theorem measurable_sum
deleted theorem measurable_swap
deleted theorem measurable_swap_iff
deleted theorem measurable_tProd_elim'
deleted theorem measurable_tProd_elim
deleted theorem measurable_tProd_mk
deleted theorem measurable_to_bool
deleted theorem measurable_to_countable'
deleted theorem measurable_to_countable
deleted theorem measurable_to_nat
deleted theorem measurable_to_prop
deleted theorem measurable_uniqueElim
deleted theorem measurable_unit
deleted theorem measurable_up
deleted theorem measurable_update'
deleted theorem measurable_update
deleted theorem measurable_updateFinset'
deleted theorem measurable_updateFinset
deleted theorem measurable_update_left
deleted theorem mem_measurableAtom_self
deleted theorem mem_of_mem_measurableAtom
added theorem ENat.measurable_iff
added theorem Measurable.and
added theorem Measurable.dite
added theorem Measurable.eq_mp
added theorem Measurable.eval
added theorem Measurable.exists
added theorem Measurable.find
added theorem Measurable.forall
added theorem Measurable.fst
added theorem Measurable.iff
added theorem Measurable.imp
added theorem Measurable.not
added theorem Measurable.or
added theorem Measurable.prod
added theorem Measurable.prodMap
added theorem Measurable.prodMk
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 MeasurableSet.tProd
added def measurableAtom
added theorem measurableAtom_subset
added theorem measurableSet_mem
added theorem measurableSet_not_mem
added theorem measurableSet_pi
added theorem measurableSet_prod
added theorem measurableSet_quotient
added theorem measurableSet_setOf
added theorem measurableSet_sum_iff
added theorem measurableSet_swap_iff
added theorem measurable_compl
added theorem measurable_down
added theorem measurable_eq_mp
added theorem measurable_find
added theorem measurable_from_nat
added theorem measurable_fst
added theorem measurable_iUnionLift
added theorem measurable_inclusion
added theorem measurable_inl
added theorem measurable_inr
added theorem measurable_liftCover
added theorem measurable_mem
added theorem measurable_piCongrLeft
added theorem measurable_pi_apply
added theorem measurable_pi_iff
added theorem measurable_pi_lambda
added theorem measurable_prod
added theorem measurable_prodMk_left
added theorem measurable_quot_mk
added theorem measurable_set_iff
added theorem measurable_set_mem
added theorem measurable_set_not_mem
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_bool
added theorem measurable_to_nat
added theorem measurable_to_prop
added theorem measurable_uniqueElim
added theorem measurable_unit
added theorem measurable_up
added theorem measurable_update'
added theorem measurable_update
added theorem measurable_update_left
added theorem MeasurableSet.coe_bot
added theorem MeasurableSet.coe_himp
added theorem MeasurableSet.coe_top
added theorem MeasurableSet.mem_coe
added theorem measurableSet_tendsto