one_lt_card_iff_nontrivial — Mathlib

English

For a finite α, one has 1 < Nat.card α if and only if α is nontrivial (has at least two distinct elements).

Русский

Для конечного α: 1 < Nat.card α тогда и только тогда, когда α не тривиален (есть по меньшей мере два различных элемента).

LaTeX

$$$1 < Nat.card(\alpha) \iff Nontrivial(\alpha)$$$

Lean4

theorem one_lt_card_iff_nontrivial [Finite α] : 1 < Nat.card α ↔ Nontrivial α :=
  by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]

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