English
Given any finite s ⊆ α and n ≥ |s|, there exists t ⊇ s with |t| = n (α infinite).
Русский
Для любого конечного s ⊆ α и n ≥ |s| существует t ⊇ s такое, что |t| = n (α бесконечно).
LaTeX
$$$ \\forall s:\\mathrm{Finset}(\\alpha),\\forall n:\\mathbb{N}, \\#s \\le n \\Rightarrow \\exists t:\\mathrm{Finset}(\\alpha), s \\subseteq t \\land \\#t = n $$$
Lean4
/-- See `Infinite.exists_subset_card_eq` for a version that provides an arbitrary
`s : Finset α` for any cardinality. -/
theorem exists_superset_card_eq [Infinite α] (s : Finset α) (n : ℕ) (hn : #s ≤ n) : ∃ t : Finset α, s ⊆ t ∧ #t = n := by
induction n generalizing s with
| zero => exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
| succ n IH =>
rcases hn.eq_or_lt with hn' | hn'
· exact ⟨s, subset_rfl, hn'⟩
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
obtain ⟨x, hx⟩ := exists_notMem_finset t
refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
simp [ht]
