AEMeasurableSequence

📁 Source: Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean

Statistics

Metric	Count
Definitions aeSeq, aeSeqSet	2
Theorems aeSeqSet_measurableSet, aeSeq_eq_fun_ae, aeSeq_eq_fun_of_mem_aeSeqSet, aeSeq_eq_mk_ae, aeSeq_eq_mk_of_mem_aeSeqSet, aeSeq_n_eq_fun_n_ae, fun_prop_of_mem_aeSeqSet, iInf, iSup, measurable, measure_compl_aeSeqSet_eq_zero, mk_eq_fun_of_mem_aeSeqSet, prop_of_mem_aeSeqSet	13
Total	15

(root)

Definitions

Name	Category	Theorems
aeSeq 📖	CompOp	7 math math: aeSeq.measurable, aeSeq.aeSeq_n_eq_fun_n_ae, aeSeq.iSup, aeSeq.aeSeq_eq_mk_of_mem_aeSeqSet, aeSeq.iInf, aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet, aeSeq.prop_of_mem_aeSeqSet
aeSeqSet 📖	CompOp	2 math math: aeSeq.aeSeqSet_measurableSet, aeSeq.measure_compl_aeSeqSet_eq_zero

aeSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeSeqSet_measurableSet 📖	mathematical	AEMeasurable	MeasurableSet aeSeqSet	—	MeasurableSet.compl MeasureTheory.measurableSet_toMeasurable
aeSeq_eq_fun_ae 📖	—	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_mono_null aeSeq_eq_fun_of_mem_aeSeqSet measure_compl_aeSeqSet_eq_zero
aeSeq_eq_fun_of_mem_aeSeqSet 📖	mathematical	AEMeasurable Set Set.instMembership aeSeqSet	aeSeq	—	aeSeq_eq_mk_of_mem_aeSeqSet mk_eq_fun_of_mem_aeSeqSet
aeSeq_eq_mk_ae 📖	—	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono MeasureTheory.ae_iff measure_compl_aeSeqSet_eq_zero
aeSeq_eq_mk_of_mem_aeSeqSet 📖	mathematical	AEMeasurable Set Set.instMembership aeSeqSet	aeSeq	—	—
aeSeq_n_eq_fun_n_ae 📖	mathematical	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq aeSeq	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff aeSeq_eq_fun_ae
fun_prop_of_mem_aeSeqSet 📖	—	AEMeasurable Set Set.instMembership aeSeqSet	—	—	aeSeq_eq_fun_of_mem_aeSeqSet prop_of_mem_aeSeqSet
iInf 📖	mathematical	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq iInf Pi.infSet aeSeq	—	MeasureTheory.Measure.instOuterMeasureClass iSup
iSup 📖	mathematical	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq iSup Pi.supSet aeSeq	—	MeasureTheory.Measure.instOuterMeasureClass iSup_apply aeSeq_eq_fun_of_mem_aeSeqSet MeasureTheory.measure_mono_null Set.compl_subset_compl measure_compl_aeSeqSet_eq_zero
measurable 📖	mathematical	AEMeasurable	Measurable aeSeq	—	Measurable.ite aeSeqSet_measurableSet measurable_const'
measure_compl_aeSeqSet_eq_zero 📖	mathematical	AEMeasurable Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	DFunLike.coe Set ENNReal Compl.compl Set.instCompl aeSeqSet instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass aeSeqSet.eq_1 compl_compl MeasureTheory.measure_toMeasurable Filter.Eventually.and
mk_eq_fun_of_mem_aeSeqSet 📖	—	AEMeasurable Set Set.instMembership aeSeqSet	—	—	aeSeqSet.eq_1 compl_compl Set.compl_subset_compl Set.Subset.trans MeasureTheory.subset_toMeasurable
prop_of_mem_aeSeqSet 📖	mathematical	AEMeasurable Set Set.instMembership aeSeqSet	aeSeq	—	mk_eq_fun_of_mem_aeSeqSet compl_compl aeSeqSet.eq_1 Set.compl_subset_compl Set.Subset.trans MeasureTheory.subset_toMeasurable Set.mem_of_subset_of_mem

---

← Back to Index