toNat_lift_add_lift — Mathlib

English

For a,b cardinals with a < aleph0 and b < aleph0, toNat(lift(a) + lift(b)) = toNat(a) + toNat(b).

Русский

Для a,b кардиналов с a < ℵ0 и b < ℵ0: toNat(lift(a) + lift(b)) = toNat(a) + toNat(b).

LaTeX

$$$\forall {a} {b} (ha : a < \aleph_0) (hb : b < \aleph_0),\ toNat(\mathrm{lift}(a) + \mathrm{lift}(b)) = toNat(a) + toNat(b).$$$

Lean4

theorem toNat_lift_add_lift {a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < ℵ₀) (hb : b < ℵ₀) :
    toNat (lift.{v} a + lift.{u} b) = toNat a + toNat b := by simp [*]

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