measure_eq_iInf_isOpen — Mathlib

English

For OuterRegular μ, there exists an open set U ⊇ A with μ(U) < μ(A) + ε when ε ≠ 0.

Русский

Для OuterRegular μ существует открытое множество U ⊇ A такое, что μ(U) < μ(A) + ε при ε ≠ 0.

LaTeX

$$$A.exists\_isOpen\_lt\_add μ ε \Rightarrow μ(U) < μ(A)+ε$$$

Lean4

/-- For an outer regular measure, the measure of a set is the infimum of the measures of open sets
containing it. -/
theorem _root_.Set.measure_eq_iInf_isOpen (A : Set α) (μ : Measure α) [OuterRegular μ] :
    μ A = ⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), μ U :=
  by
  refine le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) ?_
  refine le_of_forall_gt fun r hr => ?_
  simpa only [iInf_lt_iff, exists_prop] using A.exists_isOpen_lt_of_lt r hr

Похожие утверждения