closedBall

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

y belongs to the closed ball if and only if dist y x ≤ ε.

Русский

y принадлежит замкнутому шару тогда и только тогда, когда dist y x ≤ ε.

LaTeX

$$$ y \in \mathrm{closedBall}(x,\varepsilon) \iff dist(y,x) \le \varepsilon $$$

Lean4

/-- `closedBall x ε` is the set of all points `y` with `dist y x ≤ ε` -/
def closedBall (x : α) (ε : ℝ) :=
  {y | dist y x ≤ ε}

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

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

Разделы

Аффилиация

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