infEdist_closure_pos_iff_notMem_closure

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

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

theorem infEdist_closure_pos_iff_notMem_closure {x : α} {E : Set α} : 0 < infEdist x (closure E) ↔ x ∉ closure E := by
  rw [infEdist_closure, infEdist_pos_iff_notMem_closure]

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

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

Разделы

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

Аффилиация

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