English
If t is infinite and s ⊆ t with s finite, then for any k ≥ s.ncard there exists s' with s ⊆ s' ⊆ t and s'.ncard = k.
Русский
Если t бесконечно, и s ⊆ t конечно, то для любого k ≥ s.ncard существует s' с s ⊆ s' ⊆ t и s'.ncard = k.
LaTeX
$$$$ \forall k, (s \subseteq t) \Rightarrow (\text{exists } s' \text{ с } s \subseteq s' \subseteq t \land s'.ncard = k) $$$$
Lean4
theorem exists_superset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t) (hs : s.Finite) {k : ℕ}
(hsk : s.ncard ≤ k) : ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k :=
by
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)
refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans diff_subset), ?_⟩
rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card, add_tsub_cancel_of_le]
