English
Under the hypothesis h and with hr linking |α|.ord to type r, the cardinality of the subtype of subsets S ⊆ α with |S| < cof((|α|).ord) equals |α|.
Русский
При гипотезе h и связи hr между |α|.ord и type r кардинал множества подмножеств S ⊆ α с |S| < cof((|α|).ord) равен |α|.
LaTeX
$$$$ \left|\{ S \subseteq \alpha \mid |S| < \operatorname{cof}((|\alpha|).\operatorname{ord}) \} \right| = |\alpha|. $$$$
Lean4
theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) : #{ s : Set α // #s < cof (#α).ord } = #α :=
by
rcases eq_or_ne (#α) 0 with (ha | ha)
· simp [ha]
have h' : IsStrongLimit #α := ⟨ha, @h⟩
rcases ord_eq α with ⟨r, wo, hr⟩
apply le_antisymm
· conv_rhs => rw [← mk_bounded_subset h hr]
apply mk_le_mk_of_subset
intro s hs
rw [hr] at hs
exact lt_cof_type hs
· refine @mk_le_of_injective α _ (fun x => Subtype.mk { x } ?_) ?_
· rw [mk_singleton]
exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (isSuccLimit_ord h'.aleph0_le))
· intro a b hab
simpa [singleton_eq_singleton_iff] using hab
