infEdist_pos_iff_notMem_closure — Mathlib

English

0 < infEdist x (closure E) iff x ∉ closure E.

Русский

0 < infEdist x (closure E) тогда и только тогда, когда x не принадлежит closure E.

LaTeX

$$$0 < \infEdist x (\overline{E}) \iff x \notin \overline{E}$$$

Lean4

/-- The infimum edistance of a point to a set is positive if and only if the point is not in the
closure of the set. -/
theorem infEdist_pos_iff_notMem_closure {x : α} {E : Set α} : 0 < infEdist x E ↔ x ∉ closure E := by
  rw [mem_closure_iff_infEdist_zero, pos_iff_ne_zero]

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