card_le — Mathlib

English

If s is a finite set of elements from a finite universe α and s is intersecting, then 2|s| ≤ |α|.

Русский

Если s - конечное множество элементов из конечного множества α и оно пересекающее, то 2|s| ≤ |α|.

LaTeX

$$$2 \cdot |s| \le |\alpha|$$$

Lean4

theorem card_le [Fintype α] {s : Finset α} (hs : (s : Set α).Intersecting) : 2 * #s ≤ Fintype.card α := by
  classical
  refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
  rw [Nat.two_mul, card_disjUnion, card_map]

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