one_lt_card_iff_nontrivial — Mathlib

English

A finite α is nontrivial if it has more than one element; equivalently, card α > 1.

Русский

Конечный α не тривиален, если в нём больше одного элемента; эквивалентно card α > 1.

LaTeX

$$$1 < \\operatorname{card} \\alpha \\iff \\operatorname{Nontrivial} \\alpha$$$

Lean4

theorem one_lt_card_iff_nontrivial : 1 < card α ↔ Nontrivial α := by
  rw [← not_iff_not, not_lt, not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]

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