Theorems · Theorem · measure theory
MeasureTheory.mem_ae_iff
∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
{μ : F} {s : Set α}, s ∈ MeasureTheory.ae μ ↔ μ sᶜ = 0- Defined in
- Mathlib.MeasureTheory.OuterMeasure.AE
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement and proof · cited by 53,352
- ENNRealstatement and proof · cited by 9,879
- Filterstatement · cited by 8,121
- Compl.complstatement · cited by 2,925
- FunLikestatement and proof · cited by 2,560
- MeasureTheory.aestatement · cited by 2,352
- MeasureTheory.OuterMeasureClassstatement and proof · cited by 104
Cited by16
Results whose statement or proof uses this declaration.
- MeasureTheory.ae_eq_botproof · cited by 4
- ae_restrict_le_codiscreteWithinproof · cited by 4
- BoxIntegral.integrable_of_continuousOnproof · cited by 3
- MeasureTheory.ite_ae_eq_of_measure_compl_zeroproof · cited by 3
- BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAtproof · cited by 2
- MeasureTheory.mem_ae_iff_prob_eq_oneproof · cited by 2
- MeasureTheory.mem_map_restrict_ae_iffproof · cited by 1
- MeasureTheory.MeasurePreserving.singularPartproof · cited by 1
- MeasureTheory.Measure.MutuallySingular.disjoint_aeproof · cited by 1
- Polynomial.mahlerMeasure_le_sum_norm_coeffproof · cited by 1
- MeasureTheory.vadd_mem_aeproof · cited by 1
- mem_map_indicator_ae_iff_of_zero_notMemproof · cited by 1