closedBall

Mathlib.Analysis.InnerProductSpace.EuclideanDist

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

English

The closed ball is a closed set.

Русский

Замкнутая шаровая область является замкнутым множеством.

LaTeX

$$IsClosed (closedBall x r)$$

Lean4

/-- Closed ball w.r.t. the Euclidean distance. -/
def closedBall (x : E) (r : ℝ) : Set E :=
  {y | dist y x ≤ r}

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

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

Разделы

Аффилиация

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