one_lt_iff_nontrivial — Mathlib

English

For a type α, 1 < |α| if and only if α is nontrivial, i.e., there exist two distinct elements.

Русский

Пусть α—тип. Тогда 1 < |α| эквивалентно тому, что α не тривиален, то есть существуют два различных элемента.

LaTeX

$$$1 < |\alpha| \iff \exists a,b : \alpha, a \neq b$$$

Lean4

theorem one_lt_iff_nontrivial {α : Type u} : 1 < #α ↔ Nontrivial α := by
  rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]

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