exists_subset_card_eq — Mathlib

English

For any infinite set s and any natural n, there exists a finite subset t ⊆ s with card t = n.

Русский

Пусть s бесконечно; для любого натурального n существует конечное подмножество t ⊆ s такое, что |t| = n.

LaTeX

$$$ s\text{ Infinite} \Rightarrow \forall n:\mathbb{N}, \exists t:\mathrm{Finset}(\alpha), t \subseteq s \land t.card = n $$$

Lean4

theorem exists_subset_card_eq {s : Set α} (hs : s.Infinite) (n : ℕ) : ∃ t : Finset α, ↑t ⊆ s ∧ t.card = n :=
  ⟨((Finset.range n).map (hs.natEmbedding _)).map (Embedding.subtype _), by simp⟩

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