English
Let s be a subset of t. If the encard of s is at most k and k is at most the encard of t, then there exists an intermediate set r with s ⊆ r ⊆ t and r.encard = k.
Русский
Пусть s ⊆ t. Пусть энкарда s ≤ k ≤ энкарда t. Тогда существует множество r such that s ⊆ r ⊆ t и r.encard = k.
LaTeX
$$$\\exists r, s \\subseteq r \\land r \\subseteq t \\land r.encard = k$$$
Lean4
theorem exists_superset_subset_encard_eq {k : ℕ∞} (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :
∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k :=
by
obtain (hs | hs) := eq_or_ne s.encard ⊤
· rw [hs, top_le_iff] at hsk; subst hsk; exact ⟨s, Subset.rfl, hst, hs⟩
obtain ⟨k, rfl⟩ := exists_add_of_le hsk
obtain ⟨k', hk'⟩ := exists_add_of_le hkt
have hk : k ≤ encard (t \ s) :=
by
rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt
exact WithTop.le_of_add_le_add_right hs hkt
obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk
refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans diff_subset), ?_⟩
rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]
