Commit 2026-10-04 13:15 e2e36455

View on Github →

feat: measurability of set operations (#44274) The intersection of two measurable set-valued functions is measurable. Same for other set/finset operations, and aemeasurable versions for sets.

Estimated changes

added theorem Finset.measurable_coe
added theorem Measurable.compl
added theorem Measurable.inter
added theorem Measurable.sdiff
added theorem Measurable.symmDiff
added theorem Measurable.union
modified theorem measurable_compl
added theorem measurable_inter
added theorem measurable_sdiff
added theorem measurable_symmDiff
added theorem measurable_union
added theorem AEMeasurable.and
added theorem AEMeasurable.compl
added theorem AEMeasurable.const_eq
added theorem AEMeasurable.eq_const
added theorem AEMeasurable.exists
added theorem AEMeasurable.forall
added theorem AEMeasurable.iff
added theorem AEMeasurable.imp
added theorem AEMeasurable.inter
added theorem AEMeasurable.mem
added theorem AEMeasurable.not
added theorem AEMeasurable.or
added theorem AEMeasurable.sdiff
added theorem AEMeasurable.symmDiff
added theorem AEMeasurable.union
added theorem aemeasurable_mem
added theorem aemeasurable_set_iff
added theorem aemeasurable_to_prop