le_card_iff_exists_subset_card — Mathlib

English

For a finite set s, n ≤ |s| is equivalent to the existence of a subset t ⊆ s with |t| = n.

Русский

Для конечного множества s равенство n ≤ |s| эквивалентно существованию подмножества t ⊆ s такого что |t| = n.

LaTeX

$$$n \\le |s| \\iff \\exists t \\subseteq s, |t| = n$$$

Lean4

theorem le_card_iff_exists_subset_card : n ≤ #s ↔ ∃ t ⊆ s, #t = n :=
  by
  refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩
  exact exists_subset_card_eq h

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