instNontrivialOfNonempty — Mathlib

English

If α is nonempty and β is nontrivial, then there exist two distinct continuous maps α → β.

Русский

Если пространство α непустое, а β ненулевое, то существует как минимум две различные непрерывные карты α → β.

LaTeX

$$$\exists f_1, f_2 : C(\alpha, \beta),\; f_1 \neq f_2$$$

Lean4

instance [Nonempty α] [Nontrivial β] : Nontrivial C(α, β) :=
  ⟨let ⟨b₁, b₂, hb⟩ := exists_pair_ne β
    ⟨const _ b₁, const _ b₂, fun h => hb <| DFunLike.congr_fun h <| Classical.arbitrary α⟩⟩

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