mem_ball

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

An element y belongs to the open ball B(x,ε) if and only if dist(y,x) < ε.

Русский

Элемент y принадлежит открытому шару B(x,ε) тогда и только тогда, когда dist(y,x) < ε.

LaTeX

$$$ y \in \mathrm{ball}(x,\varepsilon) \iff dist(y,x) < \varepsilon $$$

Lean4

@[simp]
theorem mem_ball : y ∈ ball x ε ↔ dist y x < ε :=
  Iff.rfl

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

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

Разделы

Аффилиация

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