biUnion_lt_closedBall

Mathlib.Topology.MetricSpace.Pseudo.Lemmas

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

English

The union over all radii r' < r of closed balls equals the open ball of radius r centered at x.

Русский

Союз всех закрытых шаров радиуса r′ < r равен открытому шару радиуса r вокруг x.

LaTeX

$$$\bigcup_{r'

Lean4

theorem biUnion_lt_closedBall (x : α) (r : ℝ) : ⋃ r' < r, closedBall x r' = ball x r :=
  by
  ext
  rw [← not_iff_not]
  simp [forall_lt_iff_le]

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

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

Разделы

Аффилиация

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