lift_sum — Mathlib

English

The lifting operation commutes with summation: lift(sum f) = sum (i -> lift(f(i))).

Русский

Операция подъёма обращает сумму: lift(∑ f) = ∑ lift(f(i)).

LaTeX

$$$ \operatorname{lift}(\operatorname{sum} f) = \operatorname{sum} (\lambda i. \operatorname{lift}(f(i))) $$$

Lean4

@[simp]
theorem lift_sum {ι : Type u} (f : ι → Cardinal.{v}) :
    Cardinal.lift.{w} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w} (f i) :=
  Equiv.cardinal_eq <|
    Equiv.ulift.trans <|
      Equiv.sigmaCongrRight
        fun a =>
          -- Porting note: Inserted universe hint .{_,_,v} below

        Nonempty.some <| by rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]

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