English
For a subset s ⊆ α and a cardinal c, the family of subsets t ⊆ s with |t| ≤ c has cardinality at most max(|s|, ℵ0)^c.
Русский
Для подмножества s ⊆ α и кардинала c множество подмножеств t ⊆ s с |t| ≤ c имеет кардинальность не более max(|s|, ℵ0)^c.
LaTeX
$$$\\#\\{ t \\subseteq s \;|\\; \\#t \\le c \\} \\le \\max\\{\\#s, \\aleph_{0}\\}^{\\,c}$$$
Lean4
theorem mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :
#{ t : Set α // t ⊆ s ∧ #t ≤ c } ≤ max #s ℵ₀ ^ c :=
by
refine le_trans ?_ (mk_bounded_set_le s c)
refine ⟨Embedding.codRestrict _ ?_ ?_⟩
· use fun t => (↑) ⁻¹' t.1
rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h
apply Subtype.eq
dsimp only at h ⊢
refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption
rintro ⟨t, _, h2t⟩; exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t
