exists_subset_ncard_eq — Mathlib

English

If s is infinite, then for every k there exists a subset t ⊆ s with t finite and t.ncard = k.

Русский

Если s бесконечно, то для любого k существует подмножество t ⊆ s, конечное, такое что t.ncard = k.

LaTeX

$$$$ \forall k, \exists t \subseteq s, t\text{ finite} \land t.ncard = k $$$$

Lean4

theorem exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ) : ∃ t, t ⊆ s ∧ t.Finite ∧ t.ncard = k :=
  by
  have := hs.to_subtype
  obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k
  refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩
  rw [ncard_image_of_injective _ Subtype.coe_injective]
  simp

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