English
If α is infinite and c is a cardinal, the family of subsets of α of size at most c has cardinality at most |α|^c.
Русский
Если α бесконечно, и c — кардинал, то множество подмножеств α размером не более c имеет кардинальность не более |α|^c.
LaTeX
$$$\\#\\{ t \\subseteq \\alpha \\;|\\; \\#t \\le c \\} \\le |\\alpha|^{c}$$$
Lean4
theorem mk_bounded_set_le_of_infinite (α : Type u) [Infinite α] (c : Cardinal) : #{ t : Set α // #t ≤ c } ≤ #α ^ c :=
by
rw [← add_one_eq (aleph0_le_mk α)]
induction c using Cardinal.inductionOn with
| _ β
fapply mk_le_of_surjective
· intro f
use Sum.inl ⁻¹' range f
refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
apply mk_range_le
rintro ⟨s, ⟨g⟩⟩
classical
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val else Sum.inr (ULift.up 0)
apply Subtype.eq; ext x
constructor
· rintro ⟨y, h⟩
dsimp only at h
by_cases h' : ∃ z : s, g z = y
· rw [dif_pos h'] at h
cases Sum.inl.inj h
exact (Classical.choose h').2
· rw [dif_neg h'] at h
cases h
· intro h
have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
use g ⟨x, h⟩
dsimp only
rw [dif_pos this]
congr
suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
apply g.2
exact Classical.choose_spec this
