card_lt_iff_ne_univ — Mathlib

English

Let α be finite and s a Finset α. Then |s| < |α| iff s ≠ univ.

Русский

Пусть α конечно и s — Finset α. Тогда |s| < |α| эквивалентно s ≠ univ.

LaTeX

$$$\forall \alpha [Fintype \alpha], \forall s : Finset \alpha, |s| < |\alpha| \iff s \neq \mathrm{univ}$$$

Lean4

theorem card_lt_iff_ne_univ [Fintype α] (s : Finset α) : #s < Fintype.card α ↔ s ≠ Finset.univ :=
  s.card_le_univ.lt_iff_ne.trans (not_congr s.card_eq_iff_eq_univ)

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