mem_sphere_comm — Mathlib

English

In a metric space, a point lies on the sphere centered at y with radius ε if and only if the symmetric point lies on the sphere centered at x with radius ε.

Русский

Пусть а метрическое пространство. Тогда x ∈ сфера(y, ε) ⇔ y ∈ сфера(x, ε).

LaTeX

$$$ x \in \text{sphere}(y, \varepsilon) \iff y \in \text{sphere}(x, \varepsilon) $$$

Lean4

theorem mem_sphere_comm : x ∈ sphere y ε ↔ y ∈ sphere x ε := by rw [mem_sphere', mem_sphere]

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