exists_isOpen_le_add — Mathlib

English

For ENNReal-quantified ε ≠ 0, there exists open U ⊇ A with μ(U) ≤ μ(A) + ε.

Русский

Для ε ≠ 0 существуется открытое U ⊇ A такое, что μ(U) ≤ μ(A) + ε.

LaTeX

$$$\forall A,\ \varepsilon\neq 0 \Rightarrow \exists U\supseteq A, IsOpen(U) \land μ(U) \le μ(A) + ε.$$$

Lean4

theorem _root_.Set.exists_isOpen_le_add (A : Set α) (μ : Measure α) [OuterRegular μ] {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U ≤ μ A + ε :=
  by
  rcases eq_or_ne (μ A) ∞ with (H | H)
  · exact ⟨univ, subset_univ _, isOpen_univ, by simp only [H, _root_.top_add, le_top]⟩
  · rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩
    exact ⟨U, AU, U_open, hU.le⟩

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