card_compl_lt_iff_nonempty — Mathlib

English

Let α be finite and s a Finset α. Then |s^c| < |α| iff s is nonempty.

Русский

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

LaTeX

$$$\forall \alpha [Fintype \alpha], \forall s : Finset \alpha, |s^c| < |\alpha| \iff s \neq \varnothing$$$

Lean4

theorem card_compl_lt_iff_nonempty [Fintype α] [DecidableEq α] (s : Finset α) : #sᶜ < Fintype.card α ↔ s.Nonempty :=
  sᶜ.card_lt_iff_ne_univ.trans s.compl_ne_univ_iff_nonempty

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