subsingleton_of_einfsep_eq_top — Mathlib

English

If a set s has Einfsep equal to the top element, then s is subsingleton (has at most one element).

Русский

Если einfsep(s) = ∞, значит s является subsingleton (не более одной точки).

LaTeX

$$$ s.einfsep = \infty \Rightarrow s \text{ is a subsingleton} $$$

Lean4

theorem subsingleton_of_einfsep_eq_top (hs : s.einfsep = ∞) : s.Subsingleton :=
  by
  rw [einfsep_top] at hs
  exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

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