exists_real_pos_lt_infEdist_of_notMem_closure

English

If x ∉ closure E, there exists ε > 0 with ENNReal.ofReal ε < infEdist x E.

Русский

Если x не принадлежит closure E, существует ε > 0 такое, что ENNReal.ofReal(ε) < infEdist x E.

LaTeX

$$$\exists \varepsilon > 0\ \operatorname{ENNReal.ofReal}(\varepsilon) < \infEdist x E$$$

Lean4

theorem exists_real_pos_lt_infEdist_of_notMem_closure {x : α} {E : Set α} (h : x ∉ closure E) :
    ∃ ε : ℝ, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E :=
  by
  rw [← infEdist_pos_iff_notMem_closure, ENNReal.lt_iff_exists_real_btwn] at h
  rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩
  exact ⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩

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