exists_finset_le_card — Mathlib

English

For any α and n with n ≤ |α|, there exists a Finset α whose card is at least n.

Русский

Для любого множества α и натурального n, если n ≤ |α|, существует Finset α с card(s) ≥ n.

LaTeX

$$$\exists s : Finset \alpha, n \le s.card$$$

Lean4

theorem exists_finset_le_card (α : Type*) (n : ℕ) (h : n ≤ #α) : ∃ s : Finset α, n ≤ s.card :=
  by
  obtain hα | hα := finite_or_infinite α
  · let hα := Fintype.ofFinite α
    use Finset.univ
    simpa only [mk_fintype, Nat.cast_le] using h
  · obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n
    exact ⟨s, hs.ge⟩

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