Structures · Analysis
MeasureTheory.Measure.OuterRegular
A measure μ is outer regular if μ(A) = inf {μ(U) | A ⊆ U open} for a measurable set A.
This definition implies the same equality for any (not necessarily measurable) set, see
Set.measure_eq_iInf_isOpen.
- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Shape
- One type argument · adds outerRegular
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- Set.exists_isOpen_lt_of_lt
- MeasurableSet.exists_isOpen_sdiff_lt
- Set.exists_isOpen_lt_add
- MeasureTheory.Measure.OuterRegular.ext_isOpen
- Set.measure_eq_iInf_isOpen
- Set.exists_isOpen_le_add
- MeasureTheory.Measure.OuterRegular.outerRegular
- MeasureTheory.Measure.OuterRegular.comap'
- MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed
- MeasureTheory.Measure.OuterRegular.smul
- MeasureTheory.Measure.OuterRegular.map
- RealRMK.measure_le_of_isCompact_of_integral
- Besicovitch.exists_closedBall_covering_tsum_measure_le
- MeasureTheory.Measure.OuterRegular.comap
- MeasureTheory.Measure.OuterRegular.smul_nnreal
- MeasurableSet.exists_isOpen_diff_lt
- MeasureTheory.Measure.OuterRegular.ext_isOpen_isBounded
- MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact
Ancestors0
No ancestors.