Commit 2023-05-05 13:44 2ff8f30b

View on Github →

feat: port MeasureTheory.Function.AEMeasurableSequence (#3803)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean

added theorem aeSeq.aeSeqSet_measurableSet

added theorem aeSeq.aeSeq_eq_fun_ae

added theorem aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet

added theorem aeSeq.aeSeq_eq_mk_ae

added theorem aeSeq.aeSeq_eq_mk_of_mem_aeSeqSet

added theorem aeSeq.aeSeq_n_eq_fun_n_ae

added theorem aeSeq.fun_prop_of_mem_aeSeqSet

added theorem aeSeq.measurable

added theorem aeSeq.measure_compl_aeSeqSet_eq_zero

added theorem aeSeq.mk_eq_fun_of_mem_aeSeqSet

added theorem aeSeq.prop_of_mem_aeSeqSet

added theorem aeSeq.supᵢ

added def aeSeqSet