Theorems · Inductive type · measure theory
MeasureTheory.Measure.OuterRegular
{α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → PropA 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
- Cited by
- 24 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 by30
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.Regular.mapproof · cited by 9
- Set.exists_isOpen_lt_of_ltstatement and proof · cited by 7
- MeasurableSet.exists_isOpen_sdiff_ltstatement and proof · cited by 4
- Set.exists_isOpen_lt_addstatement and proof · cited by 4
- MeasureTheory.Measure.OuterRegular.ext_isOpenstatement and proof · cited by 4
- Set.exists_isOpen_le_addstatement and proof · cited by 3
- Set.measure_eq_iInf_isOpenstatement and proof · cited by 3
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closedstatement and proof · cited by 2
- MeasureTheory.Measure.OuterRegular.comap'statement and proof · cited by 2
- MeasureTheory.Measure.OuterRegular.outerRegularstatement and proof · cited by 2
- MeasureTheory.Measure.OuterRegular.smulstatement and proof · cited by 2
- MeasureTheory.Measure.Regular.smulproof · cited by 2