one_lt_card_iff_nontrivial — Mathlib

English

Let α be a type. Then 1 < card α if and only if α is nontrivial.

Русский

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

LaTeX

$$$$ 1 < \\operatorname{card} \\alpha \\ \\Longleftrightarrow\\ \\exists a,b \\in \\alpha,\\ a \\neq b. $$$$

Lean4

theorem one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ Nontrivial α :=
  by
  rw [← Cardinal.one_lt_iff_nontrivial]
  conv_rhs => rw [← Nat.cast_one]
  rw [← natCast_lt_toENat_iff]
  simp only [ENat.card, Nat.cast_one]

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