disjoint_closedBall_of_lt_infDist

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

If r < infDist x s, then the closed ball is disjoint from s.

Русский

Если r < infDist x s, то замкнутый шар вокруг x радиуса r дисjoint с s.

LaTeX

$${r ∈ \mathbb{R}} (r < \infDist x s) \Rightarrow \text{Disjoint}(\overline{B}(x,r), s)$$

Lean4

theorem disjoint_closedBall_of_lt_infDist {r : ℝ} (h : r < infDist x s) : Disjoint (closedBall x r) s :=
  disjoint_ball_infDist.mono_left <| closedBall_subset_ball h

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

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

Разделы

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

Аффилиация

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