one_lt_card_iff_nontrivial — Mathlib

English

1 < |s| is equivalent to s being nontrivial (not a subsingleton).

Русский

1 < |s| эквивалентно тому, что s не тривиально (не является пододноство).

LaTeX

$$1 < |s| ↔ s.Nontrivial$$

Lean4

theorem one_lt_card_iff_nontrivial : 1 < #s ↔ s.Nontrivial := by
  rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort, not_nontrivial_iff_subsingleton,
    card_le_one_iff_subsingleton_coe, coe_sort_coe]

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