exists_subset_card_eq — Mathlib

English

For every infinite α and every natural number n, there exists a finite subset of α of cardinality n.

Русский

Для любой бесконечной α и любого натурального числа n существует конечное подмножество α мощностью n.

LaTeX

$$$ \\forall \\alpha\\,[\\operatorname{Infinite}(\\alpha)]\\;\\forall n\\in\\mathbb{N},\\; \\exists s\\subseteq \\alpha:\\, |s|=n $$$

Lean4

/-- See `Infinite.exists_superset_card_eq` for a version that, for an `s : Finset α`,
provides a superset `t : Finset α`, `s ⊆ t` such that `#t` is fixed. -/
theorem exists_subset_card_eq (α : Type*) [Infinite α] (n : ℕ) : ∃ s : Finset α, #s = n :=
  ⟨(range n).map (natEmbedding α), by rw [card_map, card_range]⟩

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