Theorems · Inductive type · measure theory
MeasureTheory.OuterMeasureClass
(F : Type u_2) → (α : outParam (Type u_3)) → [FunLike F (Set α) ENNReal] → Prop
A mixin class saying that elements μ : F are outer measures on α.
This typeclass is used to unify some API for outer measures and measures.
- Defined in
- Mathlib.MeasureTheory.OuterMeasure.Defs
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 97 from the axioms, rests on 1,956 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- FunLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by107
Results whose statement or proof uses this declaration.
- MeasureTheory.aestatement and proof · cited by 2,352
- MeasureTheory.measure_monostatement and proof · cited by 338
- MeasureTheory.measure_emptystatement and proof · cited by 169
- MeasureTheory.ae_of_allstatement and proof · cited by 137
- MeasureTheory.measure_mono_nullstatement and proof · cited by 81
- MeasureTheory.ae_all_iffstatement and proof · cited by 70
- MeasureTheory.measure_congrstatement and proof · cited by 58
- MeasureTheory.measure_union_lestatement and proof · cited by 43
- MeasureTheory.measure_iUnion_lestatement and proof · cited by 39
- MeasureTheory.ae.congr_simpstatement and proof · cited by 39
- MeasureTheory.ae_eq_reflstatement and proof · cited by 29
- MeasureTheory.ae_iffstatement and proof · cited by 26