cardinalMk_eq_sum_lift — Mathlib

English

If for a cardinal κ, sum a κ^(β a) ≤ κ, then #(WType β) ≤ κ (restatement with lift).

Русский

Если для кардинала κ верно, что сумма по a κ^(β a) ≤ κ, то #(WType β) ≤ κ (с учётом lift).

LaTeX

$$$\forall {κ : Cardinal}, (\sum_{a:\alpha} κ^{lift( #(β a))}) \le κ \Rightarrow #(WType(β)) \le κ.$$$

Lean4

theorem cardinalMk_eq_sum_lift : #(WType β) = sum fun a ↦ #(WType β) ^ lift.{u} #(β a) :=
  (mk_congr <| equivSigma β).trans <| by simp_rw [mk_sigma, mk_arrow]; rw [lift_id'.{v, u}, lift_umax.{v, u}]

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