isClosed_closedBall

Mathlib.Analysis.InnerProductSpace.EuclideanDist

URI: https://scilib.ai/kg/mathlib#Euclidean.isClosed_closedBall

English

The closed ball is a closed set.

Русский

Замкнутая шаровая оболочка состоит из замкнутого множества.

LaTeX

$$IsClosed (closedBall x r)$$

Lean4

theorem isClosed_closedBall {x : E} {r : ℝ} : IsClosed (closedBall x r) :=
  isCompact_closedBall.isClosed

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

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

Разделы

Аффилиация

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