notMem_of_dist_lt_infDist

Mathlib.Topology.MetricSpace.HausdorffDistance

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

English

If dist(x, y) is strictly less than infDist(x, s), then y ∉ s.

Русский

Если dist(x, y) < infDist(x, s), то y ∉ s.

LaTeX

$$$\operatorname{dist}(x,y) < \infDist x s \Rightarrow y \notin s$$$

Lean4

theorem notMem_of_dist_lt_infDist (h : dist x y < infDist x s) : y ∉ s := fun hy =>
  h.not_ge <| infDist_le_dist_of_mem hy

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

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

Разделы

Аффилиация

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