BorelCantelli

📁 Source: Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_eventually_notMem, ae_finite_setOf_mem, liminf_ae_eq_of_forall_ae_eq, limsup_ae_eq_of_forall_ae_eq, measure_liminf_atTop_eq_zero, measure_liminf_cofinite_eq_zero, measure_limsup_atTop_eq_zero, measure_limsup_cofinite_eq_zero, measure_setOf_frequently_eq_zero	9
Total	9

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eventually_notMem 📖	mathematical	—	Filter.Eventually Set Set.instMembership Filter.atTop Nat.instPreorder ae	—	measure_setOf_frequently_eq_zero
ae_finite_setOf_mem 📖	mathematical	—	Filter.Eventually Set.Finite setOf Set Set.instMembership ae	—	ae_iff measure_limsup_cofinite_eq_zero Set.ext
liminf_ae_eq_of_forall_ae_eq 📖	mathematical	Filter.EventuallyEq ae	Filter.liminf Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder	—	Filter.eventuallyEq_set Filter.Eventually.mono instCountableInterFilter instCountableNat Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
limsup_ae_eq_of_forall_ae_eq 📖	mathematical	Filter.EventuallyEq ae	Filter.limsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder	—	Filter.eventuallyEq_set Filter.Eventually.mono instCountableInterFilter instCountableNat Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
measure_liminf_atTop_eq_zero 📖	mathematical	—	DFunLike.coe Set ENNReal Filter.liminf CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder instZeroENNReal	—	Nat.cofinite_eq_atTop measure_liminf_cofinite_eq_zero instCountableNat instInfiniteNat
measure_liminf_cofinite_eq_zero 📖	mathematical	—	DFunLike.coe Set ENNReal Filter.liminf CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.cofinite instZeroENNReal	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd measure_limsup_cofinite_eq_zero measure_mono Filter.liminf_le_limsup Filter.cofinite_neBot Filter.isBounded_le_of_top Filter.isBounded_ge_of_bot
measure_limsup_atTop_eq_zero 📖	mathematical	—	DFunLike.coe Set ENNReal Filter.limsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder instZeroENNReal	—	Nat.cofinite_eq_atTop measure_limsup_cofinite_eq_zero instCountableNat
measure_limsup_cofinite_eq_zero 📖	mathematical	—	DFunLike.coe Set ENNReal Filter.limsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.cofinite instZeroENNReal	—	bot_unique ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot Finset.isDirected_le ENNReal.tendsto_tsum_compl_atTop_zero measure_mono Filter.HasBasis.limsup_eq_iInf_iSup Filter.hasBasis_cofinite Set.iUnion_subtype Set.iInter₂_subset Finset.finite_toSet measure_iUnion_le Subtype.countable
measure_setOf_frequently_eq_zero 📖	mathematical	—	DFunLike.coe Set ENNReal setOf Filter.Frequently Filter.atTop Nat.instPreorder instZeroENNReal	—	instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Set.setOf_forall Set.setOf_exists Filter.limsup_eq_iInf_iSup_of_nat measure_limsup_atTop_eq_zero

---

← Back to Index