Structures · Analysis
MeasureTheory.OuterMeasureClass
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
- Shape
- 2 explicit arguments · adds measure_empty, measure_mono, measure_iUnion_nat_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- MeasureTheory.Measure
- MeasureTheory.OuterMeasure
How is a type an instance?
Loading the hierarchy index…
Assumed by100
- MeasureTheory.ae
- MeasureTheory.measure_mono
- MeasureTheory.measure_empty
- MeasureTheory.ae_of_all
- MeasureTheory.measure_mono_null
- MeasureTheory.ae_all_iff
- MeasureTheory.measure_congr
- MeasureTheory.measure_union_le
- MeasureTheory.measure_iUnion_le
- MeasureTheory.ae.congr_simp
- MeasureTheory.ae_eq_refl
- MeasureTheory.ae_iff
- MeasureTheory.ae_eq_empty
- MeasureTheory.mem_ae_iff
- MeasureTheory.ae_eq_set_inter
- MeasureTheory.measure_sdiff_null
- MeasureTheory.ae_le_set
- MeasureTheory.measure_iUnion_null_iff
- MeasureTheory.measure_biUnion_null_iff
- MeasureTheory.measure_eq_zero_iff_ae_notMem
- MeasureTheory.ae_eq_univ
- MeasureTheory.measure_biUnion_finset_le
- MeasureTheory.ae_ball_iff
- MeasureTheory.compl_mem_ae_iff
- MeasureTheory.measure_le_inter_add_sdiff
- MeasureTheory.measure_iUnion_null
- MeasureTheory.ae_eq_set
- MeasureTheory.measure_mono_ae
- MeasureTheory.measure_union_null
- MeasureTheory.measure_null_of_locally_null
- MeasureTheory.ae_eq_rfl
- MeasureTheory.ae_eq_set_union
- MeasureTheory.frequently_ae_mem_iff
- MeasureTheory.union_ae_eq_right_of_ae_eq_empty
- MeasureTheory.ae_eq_symm
- MeasureTheory.ae_eq_top
- MeasureTheory.pos_mono
- MeasureTheory.union_ae_eq_left_of_ae_eq_empty
- MeasureTheory.sdiff_ae_eq_self
- MeasureTheory.measure_iUnion_fintype_le
- MeasureTheory.ae_eventually_notMem
- MeasureTheory.measure_symmDiff_eq_zero_iff
- MeasureTheory.measure_setOfPred_frequently_eq_zero
- MeasureTheory.sdiff_null_ae_eq_self
- MeasureTheory.ae_eq_trans
- MeasureTheory.measure_limsup_cofinite_eq_zero
- MeasureTheory.measure_biUnion_le
- Filter.EventuallyLE.measure_le
- MeasureTheory.union_ae_eq_right
- MeasureTheory.measure_iUnion_of_tendsto_zero
Ancestors0
No ancestors.