sphere_eq_empty_of_subsingleton — Mathlib

English

If the ambient space is a subsingleton, and ε ≠ 0, then the sphere x ε is empty.

Русский

Если пространство является одиночным, и ε ≠ 0, то сфера x ε пустая.

LaTeX

$$$[\\text{Subsingleton } \\alpha] \\; (\\varepsilon \\neq 0) \\Rightarrow \\mathrm{sphere}(x, \\varepsilon) = \\emptyset$$$

Lean4

theorem sphere_eq_empty_of_subsingleton [Subsingleton α] (hε : ε ≠ 0) : sphere x ε = ∅ :=
  Set.eq_empty_iff_forall_notMem.mpr fun _ h => ne_of_mem_sphere h hε (Subsingleton.elim _ _)

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