English
If x is outside the closure of E, then there exists ε > 0 such that for all δ with 0 < δ < ε, x does not belong to the closed δ-thickening of E.
Русский
Если x не принадлежит замыканию E, то существует ε > 0, такое что для всех δ с 0 < δ < ε выполняется x ∉ cthickening δ E.
LaTeX
$$$ x \notin closure(E) \;\Rightarrow\; \exists \varepsilon > 0\;\forall 0 < δ < \varepsilon,\ x \notin cthickening δ E $$$
Lean4
/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
closed `δ`-thickening of `E` for small enough positive `δ`. -/
theorem eventually_notMem_cthickening_of_infEdist_pos {E : Set α} {x : α} (h : x ∉ closure E) :
∀ᶠ δ in 𝓝 (0 : ℝ), x ∉ Metric.cthickening δ E :=
by
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_notMem_closure h
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
simp only [cthickening, mem_setOf_eq, not_le]
exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt
