infDist_pos_iff_notMem_closure

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#Metric.infDist_pos_iff_notMem_closure

← MathLib Explorer

English

If x belongs to the closure of s, then infDist x s = 0.

Русский

Если x принадлежит замыканию s, то infDist x s = 0.

LaTeX

$$$x \in closure s \Rightarrow infDist x s = 0$$$

Lean4

theorem infDist_pos_iff_notMem_closure (hs : s.Nonempty) : x ∉ closure s ↔ 0 < infDist x s :=
  (mem_closure_iff_infDist_zero hs).not.trans infDist_nonneg.lt_iff_ne'.symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru