Structures · Analysis
MeasureTheory.Measure.WeaklyRegular
A measure μ is weakly regular if
- it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable;
- it is inner regular for open sets, using closed sets:
μ(U) = sup {μ(F) | F ⊆ U closed} for U open.
- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Shape
- One type argument · adds innerRegular
Extends1
Extended by0
Nothing extends this class yet.
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 by31
- MeasureTheory.Measure.WeaklyRegular.innerRegular
- MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable
- MeasurableSet.exists_isClosed_sdiff_lt
- MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le
- MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge
- MeasureTheory.Lp.boundedContinuousFunction_dense
- ContinuousMap.toLp_denseRange
- MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt
- MeasurableSet.exists_isClosed_lt_add
- MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le
- MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge
- MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable
- MeasureTheory.exists_upperSemicontinuous_le_lintegral_le
- MeasureTheory.exists_upperSemicontinuous_le_integral_le
- MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le
- MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge
- MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal
- BoundedContinuousFunction.toLp_denseRange
- MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top
- MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le
- MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le
- MeasurableSet.measure_eq_iSup_isClosed_of_ne_top
- MeasurableSet.exists_isClosed_diff_lt
- MeasureTheory.Measure.WeaklyRegular.smul_nnreal
- IsOpen.measure_eq_iSup_isClosed
- MeasureTheory.exists_upperSemicontinuous_lt_integral_gt
- MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure
- MeasurableSet.exists_lt_isClosed_of_ne_top
- IsOpen.exists_lt_isClosed
- MeasureTheory.Measure.WeaklyRegular.toOuterRegular
- MeasureTheory.Measure.WeaklyRegular.smul