mem_sphere — Mathlib

English

Let (α, d) be a metric space. A point y lies on the sphere of center x and radius ε if and only if the distance between y and x equals ε.

Русский

Пусть (α, d) — метрическое пространство. Точка y принадлежит сфере с центром в x и радиусом ε тогда и только тогда, когда расстояние d(y, x) равно ε.

LaTeX

$$$y \\in \\mathrm{sphere}(x, \\varepsilon) \\iff \\operatorname{dist}(y, x) = \\varepsilon$$$

Lean4

@[simp]
theorem mem_sphere : y ∈ sphere x ε ↔ dist y x = ε :=
  Iff.rfl

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