sphere_union_ball

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

The union of the sphere and the ball equals the closed ball.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sphere_union_ball : sphere x ε ∪ ball x ε = closedBall x ε := by rw [union_comm, ball_union_sphere]

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

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

Разделы

Аффилиация

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