Theorems · Theorem · measure theory
MeasureTheory.ae_eq_univ
∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
{μ : F} {s : Set α}, s =ᵐ[μ] Set.univ ↔ μ sᶜ = 0- Defined in
- Mathlib.MeasureTheory.OuterMeasure.AE
- Cited by
- 10 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.
Cites10
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
- Set.univstatement · cited by 3,945
- Compl.complstatement · cited by 2,925
- FunLikestatement and proof · cited by 2,560
- MeasureTheory.aestatement · cited by 2,352
- Filter.EventuallyEqstatement · cited by 1,912
- MeasureTheory.OuterMeasureClassstatement and proof · cited by 104
- Filter.eventuallyEq_univproof · cited by 9
Cited by10
Results whose statement or proof uses this declaration.
- NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integralproof · cited by 2
- MeasureTheory.ae_bdd_norm_condExp_of_ae_bdd_normproof · cited by 2
- ae_eq_const_or_exists_average_ne_complproof · cited by 2
- ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mulproof · cited by 1
- MeasureTheory.measure_iInter_of_ae_monotoneproof · cited by 1
- IsClosed.ae_eq_univ_iff_eqproof · cited by 1
- Convex.average_mem_interior_of_setproof · cited by 0
- MeasureTheory.ae_bdd_abs_condExp_of_ae_bdd_absproof · cited by 0
- AddAction.aestabilizer_univproof · cited by 0
- MeasureTheory.integral_eq_setIntegralproof · cited by 0