Structures · Analysis
MeasureTheory.Measure.InnerRegularCompactLTTop
A measure μ is inner regular for finite measure sets with respect to compact sets:
for any measurable set s with finite measure, then μ(s) = sup {μ(K) | K ⊆ s compact}.
The main interest of this class is that it is satisfied for both natural Haar measures (the
regular one and the inner regular one).
- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Shape
- One type argument · adds innerRegular
Extends0
Extends nothing: this is a root of the hierarchy.
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 by57
- MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular
- MeasurableSet.exists_isCompact_isClosed_sdiff_lt
- MeasurableSet.exists_lt_isCompact_of_ne_top
- MeasurableSet.measure_eq_iSup_isCompact_of_ne_top
- MeasureTheory.eventually_nhds_one_measure_smul_sdiff_lt
- MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top
- MeasureTheory.isClosed_setOfPred_preimage_ae_eq
- IsCompact.exists_isOpen_lt_of_lt
- IsCompact.exists_isOpen_lt_add
- MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top
- MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top
- MeasurableSet.exists_isCompact_lt_add
- MeasureTheory.eventually_nhds_zero_measure_vadd_sdiff_lt
- MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero
- Filter.Tendsto.compMeasurePreservingLp
- MeasureTheory.Measure.isEverywherePos_everywherePosSubset_of_measure_ne_top
- MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous
- MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt
- MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup
- MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group
- MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
- ContinuousWithinAt.compMeasurePreservingLp
- MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant
- MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group
- MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
- IsOpen.measure_eq_biSup_integral_continuous
- MeasurableSet.exists_isCompact_isClosed_lt_add
- MeasureTheory.tendsto_measure_smul_sdiff_isCompact_isClosed
- MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top
- MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup
- MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariant
- MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure
- ContinuousAt.compMeasurePreservingLp
- MeasurableSet.exists_isCompact_sdiff_lt
- MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top
- MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure
- MeasureTheory.Lp.compMeasurePreserving_continuous
- MeasurableSet.exists_isOpen_symmDiff_lt
- MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure
- MeasureTheory.Lp.instContinuousVAddDomAddAct
- MeasureTheory.Measure.InnerRegularCompactLTTop.instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure
- MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal
- IsCompact.measure_eq_iInf_isOpen
- MeasurableSet.exists_isCompact_isClosed_diff_lt
- MeasureTheory.Measure.InnerRegularCompactLTTop.restrict
- MeasurableSet.exists_isCompact_diff_lt
- MeasureTheory.tendsto_measure_vadd_sdiff_isCompact_isClosed
- MeasureTheory.isClosed_setOf_preimage_ae_eq
- MeasureTheory.Measure.InnerRegularCompactLTTop.instInnerRegularOfIsFiniteMeasure
- MeasureTheory.Measure.InnerRegularCompactLTTop.smul
Ancestors0
No ancestors.