English
Given k ≤ s.encard, there exists t ⊆ s with t.encard = k.
Русский
При k ≤ s.encard существует подмножество t ⊆ s такое, что t.encard = k.
LaTeX
$$$\\exists t, t \\subseteq s \\land t.encard = k$$$
Lean4
theorem exists_subset_encard_eq {k : ℕ∞} (hk : k ≤ s.encard) : ∃ t, t ⊆ s ∧ t.encard = k := by
induction k using ENat.nat_induction with
| zero => exact ⟨∅, empty_subset _, by simp⟩
| succ n IH =>
obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
simp only [Nat.cast_succ] at *
have hne : t₀ ≠ s := by rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
| top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
