English
Given s ⊆ t and bounds n between s.ncard and t.ncard, there exists u with s ⊆ u ⊆ t and u.ncard = n.
Русский
При наличии s ⊆ t и некоторой кардинальности n между s.ncard и t.ncard существует множество u с s ⊆ u ⊆ t и u.ncard = n.
LaTeX
$$$$ s \subseteq t \land s.ncard \le n \land n \le t.ncard \Rightarrow \exists u: \; s \subseteq u \subseteq t \land u.ncard = n $$$$
Lean4
/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
set `u` of size `n` which is both a superset of `s` and a subset of `t`. -/
theorem exists_subsuperset_card_eq {n : ℕ} (hst : s ⊆ t) (hsn : s.ncard ≤ n) (hnt : n ≤ t.ncard) :
∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n := by
obtain ht | ht := t.infinite_or_finite
· rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt
exact ⟨t, hst, Subset.rfl, hnt.symm⟩
lift s to Finset α using ht.subset hst
lift t to Finset α using ht
obtain ⟨u, hsu, hut, hu⟩ := Finset.exists_subsuperset_card_eq (mod_cast hst) (by simpa using hsn) (mod_cast hnt)
exact ⟨u, mod_cast hsu, mod_cast hut, mod_cast hu⟩
