English
If h says that for all x with x < |α|, 2^x < |α|, and the well-order r has type |α|, then the collection of r-bounded subsets of α has the same cardinality as α.
Русский
Если для каждого x < |α| выполнено 2^x < |α|, и тип r равен ord(α), то семейство подмножеств α, ограниченных по r, имеет кардинал |α|.
LaTeX
$$$$ \Big|\{ S \subseteq \alpha \mid Bounded_r(S) \}\Big| = |\alpha|. $$$$
Lean4
theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop} [IsWellOrder α r]
(hr : (#α).ord = type r) : #{ s : Set α // Bounded r s } = #α :=
by
rcases eq_or_ne (#α) 0 with (ha | ha)
· rw [ha]
haveI := mk_eq_zero_iff.1 ha
rw [mk_eq_zero_iff]
constructor
rintro ⟨s, hs⟩
exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)
have h' : IsStrongLimit #α := ⟨ha, @h⟩
have ha := h'.aleph0_le
apply le_antisymm
· have : {s : Set α | Bounded r s} = ⋃ i, 𝒫{j | r j i} := setOf_exists _
rw [← coe_setOf, this]
refine
mk_iUnion_le_sum_mk.trans
((sum_le_iSup (fun i => #(𝒫{j | r j i}))).trans ((mul_le_max_of_aleph0_le_left ha).trans ?_))
rw [max_eq_left]
apply ciSup_le' _
intro i
rw [mk_powerset]
apply (h'.two_power_lt _).le
rw [coe_setOf, card_typein, ← lt_ord, hr]
apply typein_lt_type
· refine @mk_le_of_injective α _ (fun x => Subtype.mk { x } ?_) ?_
· apply bounded_singleton
rw [← hr]
apply isSuccLimit_ord ha
· intro a b hab
simpa [singleton_eq_singleton_iff] using hab
