Theorems · Inductive type · measure theory
MeasureTheory.Measure.InnerRegular
{α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → PropA measure μ is inner regular if, for any measurable set s, then
μ(s) = sup {μ(K) | K ⊆ s compact}.
- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by51
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.InnerRegular.innerRegularstatement and proof · cited by 7
- aeconst_of_dense_setOfPred_preimage_smul_aestatement and proof · cited by 4
- aeconst_of_dense_setOfPred_preimage_vadd_aestatement and proof · cited by 4
- MeasurableSet.measure_eq_iSup_isCompactstatement and proof · cited by 4
- aeconst_of_dense_setOfPred_preimage_smul_eqstatement and proof · cited by 3
- aeconst_of_dense_setOfPred_preimage_vadd_eqstatement and proof · cited by 3
- isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_leproof · cited by 2
- MeasureTheory.Measure.InnerRegular.map_iffstatement and proof · cited by 2
- MeasureTheory.Measure.InnerRegular.map_of_continuousstatement and proof · cited by 2
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegularstatement and proof · cited by 2
- MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegularstatement and proof · cited by 2
- MeasurableSet.exists_lt_isCompactstatement and proof · cited by 2