ball_infDist_compl_subset

Mathlib.Topology.MetricSpace.HausdorffDistance

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

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_compl_subset : ball x (infDist x sᶜ) ⊆ s :=
  ball_infDist_subset_compl.trans_eq (compl_compl s)

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

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

Разделы

Аффилиация

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