mem_closedBall

Mathlib.Topology.EMetricSpace.Defs

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

English

Same equality for membership: y ∈ closedBall x ε ↔ edist y x ≤ ε.

Русский

Та же эквивалентность для принадлежности: y ∈ closedBall(x,ε) ⇔ edist(y,x) ≤ ε.

LaTeX

$$$ y \in \operatorname{closedBall}(x,\varepsilon) \iff \operatorname{edist}(y,x) \le \varepsilon. $$$

Lean4

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

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

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

Разделы

Аффилиация

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