instOfNonemptyOfSubsingleton — Mathlib

English

If a space Y is nonempty and subsingleton, then Y is contractible.

Русский

Если пространство Y непусто и имеет не более одного элемента, то Y конрактно.

LaTeX

$$$[\text{Nonempty }Y]\,[\text{Subsingleton }Y]\Rightarrow \operatorname{ContractibleSpace}(Y).$$$

Lean4

instance [Nonempty Y] [Subsingleton Y] : ContractibleSpace Y :=
  let ⟨_⟩ := nonempty_unique Y
  ⟨⟨(Homeomorph.homeomorphOfUnique Y Unit).toHomotopyEquiv⟩⟩

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