Theorems · Theorem · measure theory
MeasurableSet.exists_isOpen_sdiff_lt
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.OuterRegular]
{A : Set α}, MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- MeasurableSetstatement and proof · cited by 3,075
- IsOpenstatement and proof · cited by 2,400
- LT.lt.trans_leproof · cited by 678
- le_topproof · cited by 411
- MeasurableSet.nullMeasurableSetproof · cited by 155
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpenproof · cited by 2
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closedproof · cited by 2
- BoxIntegral.hasIntegralIndicatorConstproof · cited by 1
- MeasurableSet.exists_isOpen_diff_ltproof · cited by 0