mem_closedBall'

Mathlib.Topology.EMetricSpace.Defs

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

English

Open phrasing of the previous equality: y ∈ closedBall x ε ↔ edist x y ≤ ε.

Русский

Открытая формулировка предыдущего равенства: y ∈ closedBall(x,ε) ⇔ edist(x,y) ≤ ε.

LaTeX

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

Lean4

theorem mem_closedBall' : y ∈ closedBall x ε ↔ edist x y ≤ ε := by rw [edist_comm, mem_closedBall]

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

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

Разделы

Аффилиация

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