sphere

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

The sphere sphere(x,ε) is the set of all points y with dist y x = ε.

Русский

Сфера sphere(x,ε) — множество точек y с dist(y,x) = ε.

LaTeX

$$$ \mathrm{sphere}(x,\varepsilon) = \{ y \in \alpha : dist(y,x) = \varepsilon \} $$$

Lean4

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

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

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

Разделы

Аффилиация

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