cardinalMk_eq_sum — Mathlib

English

If for all a, the inequality holds, then #(WType β) ≤ κ, i.e., WType is bounded by κ under the componentwise bound.

Русский

Если для всех a выполняется неравенство, то #(WType β) ≤ κ; WType ограничено κ компонентно.

LaTeX

$$$\forall {\kappa}, \big( \sum_{a:\alpha} (\kappa ^ #(β a)) \le \kappa \big) \Rightarrow #(WType(β)) \le \kappa.$$$

Lean4

theorem cardinalMk_eq_sum : #(WType β) = sum (fun a : α => #(WType β) ^ #(β a)) :=
  cardinalMk_eq_sum_lift.trans <| by simp_rw [lift_id]

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