cardinalMk_le_of_le — Mathlib

English

The same upper bound with a lifted interpretation: if the sum ≤ κ, then # (WType β) ≤ κ.

Русский

Та же верхняя граница с подъемом: если сумма ≤ κ, то #(WType β) ≤ κ.

LaTeX

$$$#(WType(β)) ≤ κ \Leftarrow (\sum_{a:\alpha} κ ^ #(β a)) ≤ κ.$$$

Lean4

/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
theorem cardinalMk_le_of_le {κ : Cardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) : #(WType β) ≤ κ :=
  cardinalMk_le_of_le' <| by simp_rw [lift_id]; exact hκ

Похожие утверждения