exists_isOpen_lt_add — Mathlib

English

For OuterRegular μ, there exists open U ⊇ A with μ(U) ≤ μ(A) + ε.

Русский

Для OuterRegular μ существует открытое U ⊇ A с μ(U) ≤ μ(A) + ε.

LaTeX

$$$A.exists\_isOpen\_le\_add μ ε \Rightarrow ∃ U, U \supseteq A, IsOpen(U) ∧ μ(U) ≤ μ(A) + ε$$$

Lean4

theorem _root_.Set.exists_isOpen_lt_add [OuterRegular μ] (A : Set α) (hA : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < μ A + ε :=
  A.exists_isOpen_lt_of_lt _ (ENNReal.lt_add_right hA hε)

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