Structures · Analysis
MeasureTheory.Measure.InnerRegular
A measure μ is inner regular if, for any measurable set s, then
μ(s) = sup {μ(K) | K ⊆ s compact}.
- 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 by62
- MeasureTheory.Measure.InnerRegular.innerRegular
- MeasurableSet.measure_eq_iSup_isCompact
- aeconst_of_dense_setOfPred_preimage_vadd_ae
- aeconst_of_dense_setOfPred_preimage_smul_ae
- aeconst_of_dense_setOfPred_preimage_smul_eq
- aeconst_of_dense_setOfPred_preimage_vadd_eq
- MeasurableSet.exists_lt_isCompact
- MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular
- MeasureTheory.Measure.InnerRegular.map_of_continuous
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular
- ergodic_add_left_iff_denseRange_zsmul
- ergodic_smul_of_denseRange_pow
- ergodic_smul_of_denseRange_zpow
- aeconst_of_dense_aestabilizer_smul
- ergodic_vadd_of_denseRange_zsmul
- MeasureTheory.Measure.InnerRegular.map
- ergodic_vadd_of_denseRange_nsmul
- MeasureTheory.Measure.support_mem_ae_of_innerRegular
- ergodic_mul_left_of_denseRange_zpow
- MeasureTheory.Measure.InnerRegular.comap'
- MonoidHom.preErgodic_of_dense_iUnion_preimage_one
- ergodic_add_left_of_denseRange_zsmul
- aeconst_of_dense_aestabilizer_vadd
- MeasureTheory.Measure.everywherePosSubset_ae_eq
- AddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero
- aeconst_of_dense_setOf_preimage_smul_eq
- MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular
- ergodic_mul_left_of_denseRange_pow
- MeasureTheory.innerRegular_map_mul_right
- MeasureTheory.Measure.InnerRegular.neg
- MeasureTheory.Measure.InnerRegular.smul
- MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular
- MeasureTheory.Measure.InnerRegular.instSum_1
- aeconst_of_dense_setOf_preimage_smul_ae
- MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular
- MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos
- MeasureTheory.Measure.InnerRegular.comap
- ErgodicSMul.trans_isMinimal
- ergodic_mul_left_iff_denseRange_zpow
- MeasureTheory.innerRegular_map_vadd
- MeasureTheory.Measure.InnerRegular.instSum
- MeasureTheory.isTightMeasureSet_singleton_of_innerRegular
- MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos
- aeconst_of_dense_setOf_preimage_vadd_eq
- MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop
- MeasureTheory.Measure.isEverywherePos_everywherePosSubset
- MeasureTheory.Measure.InnerRegular.inv
- MeasureTheory.Measure.InnerRegular.exists_isCompact_not_null
- MeasureTheory.innerRegular_map_add_left
- MeasureTheory.innerRegular_map_mul_left
Ancestors0
No ancestors.