notMem_iff_infDist_pos — Mathlib

English

For a closed set, x ∉ s if and only if infDist x s > 0, assuming s is nonempty.

Русский

Пусть s замкнуто и непусто: x ∉ s ⇔ infDist x s > 0.

LaTeX

$$$s \text{ closed},\ s \neq \varnothing \Rightarrow (x \notin s \iff 0 < infDist x s)$$$

Lean4

/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes. -/
theorem _root_.IsClosed.notMem_iff_infDist_pos (h : IsClosed s) (hs : s.Nonempty) : x ∉ s ↔ 0 < infDist x s := by
  simp [h.mem_iff_infDist_zero hs, infDist_nonneg.lt_iff_ne']

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