English
The cardinality of WType β equals the sum over a of the cardinality of WType β raised to the cardinality of β a, with a lift on the exponent.
Русский
Кардинал(WType β) равен сумме по a от кардинала(WType β) в степень кардинала(β a), с учетом подъема показателя.
LaTeX
$$$#(WType(β)) = \sum_{a:α} #(WType(β))^{ lift(#(β a)) }$$$
Lean4
/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
theorem cardinalMk_le_of_le' {κ : Cardinal.{max u v}} (hκ : (sum fun a : α => κ ^ lift.{u} #(β a)) ≤ κ) :
#(WType β) ≤ κ :=
by
induction κ using Cardinal.inductionOn with
| _ γ
simp_rw [← lift_umax.{v, u}] at hκ
nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ
simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ
obtain ⟨hκ⟩ := hκ
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
