mem_closedBall

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

y ∈ closedBall x ε iff dist y x ≤ ε (alternate form).

Русский

y ∈ closedBall x ε ⇔ dist y x ≤ ε (альтернативная форма).

LaTeX

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

Lean4

@[simp]
theorem mem_closedBall : y ∈ closedBall x ε ↔ dist y x ≤ ε :=
  Iff.rfl

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

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

Разделы

Аффилиация

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