mem_iff_infDist_zero — Mathlib

English

If s is closed and nonempty, then x ∈ s iff infDist x s = 0.

Русский

Если s замкнуто и непусто, тогда x ∈ s тогда и только тогда infDist x s = 0.

LaTeX

$$$\text{IsClosed}(s) \Rightarrow s \neq \varnothing \Rightarrow (x \in s \iff infDist x s = 0)$$$

Lean4

/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
theorem _root_.IsClosed.mem_iff_infDist_zero (h : IsClosed s) (hs : s.Nonempty) : x ∈ s ↔ infDist x s = 0 := by
  rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]

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