mem_ball'

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

Opening ball membership remains equivalent when swapping arguments: y ∈ ball x ε iff dist x y < ε.

Русский

Членство в шаре сохраняется при перестановке аргументов: y ∈ ball x ε ⇔ dist x y < ε.

LaTeX

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

Lean4

theorem mem_ball' : y ∈ ball x ε ↔ dist x y < ε := by rw [dist_comm, mem_ball]

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

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

Разделы

Аффилиация

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