sphere_isEmpty_of_subsingleton — Mathlib

English

In a subsingleton metric space, the sphere with nonzero radius is empty.

Русский

В метрическом пространстве-подпустых точек сфера с ненулевым радиусом пустая.

LaTeX

$$If $\\alpha$ is a Subsingleton and $\\varepsilon \\neq 0$, then $\\mathrm{sphere}(x,\\varepsilon)$ is empty.$$

Lean4

instance sphere_isEmpty_of_subsingleton [Subsingleton α] [NeZero ε] : IsEmpty (sphere x ε) := by
  rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]; infer_instance

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