mem_iff_infEdist_zero_of_closed

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#EMetric.mem_iff_infEdist_zero_of_closed

← MathLib Explorer

English

Same as above: x ∈ closure s iff infEdist x s = 0.

Русский

То же самое: x ∈ closure s ↔ infEdist x s = 0.

LaTeX

$$$x \in \overline{s} \iff \infEdist x s = 0$$$

Lean4

/-- Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes -/
theorem mem_iff_infEdist_zero_of_closed (h : IsClosed s) : x ∈ s ↔ infEdist x s = 0 := by
  rw [← mem_closure_iff_infEdist_zero, h.closure_eq]

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

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

Разделы

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

Аффилиация

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