ball_infDist_subset_compl

Mathlib.Topology.MetricSpace.HausdorffDistance

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

English

The open ball around x with radius infDist(x, s^c) is contained in s.

Русский

Открытый шар вокруг x радиуса infDist(x, s^c) содержится в s.

LaTeX

$$$Ball(x, \infDist x\,s^c) \subseteq s$$$

Lean4

theorem ball_infDist_subset_compl : ball x (infDist x s) ⊆ sᶜ :=
  (disjoint_ball_infDist (s := s)).subset_compl_right

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

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

Разделы

Аффилиация

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