eventually_notMem_thickening_of_infEdist_pos

English

If x ∉ closure(E), then for δ small enough with δ > 0, x ∉ thickening δ E.

Русский

Если x ∉ замыкания(E), то для достаточно малого, положительного δ, x не принадлежит thickening δ E.

LaTeX

$$$x\\notin closure(E) \\Rightarrow ∀^\\!_{δ\\to 0^+} x \\notin thickening\\,δ\\,E$$$

Lean4

/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
(open) `δ`-thickening of `E` for small enough positive `δ`. -/
theorem eventually_notMem_thickening_of_infEdist_pos {E : Set α} {x : α} (h : x ∉ closure E) :
    ∀ᶠ δ in 𝓝 (0 : ℝ), x ∉ Metric.thickening δ E :=
  by
  obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_notMem_closure h
  filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
  simp only [thickening, mem_setOf_eq, not_lt]
  exact (ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le

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