instNontrivial — Mathlib

English

An infinite type is nontrivial; there exist two distinct elements.

Русский

Бесконечный тип ненулевой; существуют два разных элемента.

LaTeX

$$∀ α [Infinite α], Nontrivial α$$

Lean4

instance (priority := 100) (α : Type*) [Infinite α] : Nontrivial α :=
  ⟨let ⟨x, _hx⟩ := exists_notMem_finset (∅ : Finset α)
    let ⟨y, hy⟩ := exists_notMem_finset ({ x } : Finset α)
    ⟨y, x, by simpa only [mem_singleton] using hy⟩⟩

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