ball_union_sphere

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

The union of the open ball and the sphere is equal to the closed ball.

Русский

Объединение открытого шара и сферы равно замкнутому шару.

LaTeX

$$ball(x,ε) ∪ sphere(x,ε) = closedBall(x,ε)$$

Lean4

@[simp]
theorem ball_union_sphere : ball x ε ∪ sphere x ε = closedBall x ε :=
  Set.ext fun _y => (@le_iff_lt_or_eq ℝ _ _ _).symm

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

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

Разделы

Аффилиация

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