English
The cardinality of WType β equals the sum over a of the cardinality of WType β raised to the cardinality of β a (without lift).
Русский
Кардинал(WType β) равен сумма по a от кардинала(WType β) в степень кардинала(β a) (без lift).
LaTeX
$$$#(WType(β)) = \sum_{a:\alpha} #(WType(β))^{ #(β a) }$$$
Lean4
/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀` -/
theorem cardinalMk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] : #(WType β) ≤ max (lift.{v} #α) ℵ₀ :=
(isEmpty_or_nonempty α).elim
(by
intro h
rw [Cardinal.mk_eq_zero (WType β)]
exact zero_le _)
fun hn =>
let m := max (lift.{v} #α) ℵ₀
cardinalMk_le_of_le' <|
calc
(Cardinal.sum fun a => m ^ lift.{u} #(β a)) ≤ lift.{v} #α * ⨆ a, m ^ lift.{u} #(β a) :=
Cardinal.sum_le_iSup_lift _
_ ≤ m * ⨆ a, m ^ lift.{u} #(β a) := (mul_le_mul' (le_max_left _ _) le_rfl)
_ = m :=
mul_eq_left (le_max_right _ _) (ciSup_le' fun _ => pow_le (le_max_right _ _) (lt_aleph0_of_finite _)) <|
pos_iff_ne_zero.1 <|
Order.succ_le_iff.1
(by
rw [succ_zero]
obtain ⟨a⟩ : Nonempty α := hn
refine le_trans ?_ (le_ciSup (bddAbove_range _) a)
rw [← power_zero]
exact power_le_power_left (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _))
