closedBall_diff_sphere

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

← MathLib Explorer

English

The difference closedBall x ε \ sphere x ε equals ball x ε.

Русский

Разность замкнутого шара и сферы равна открытому шару.

LaTeX

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

Lean4

@[simp]
theorem closedBall_diff_sphere : closedBall x ε \ sphere x ε = ball x ε := by
  rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]

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

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

Разделы

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

Аффилиация

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