lift_prod — Mathlib

English

Lifting commutes with finite products: lift(prod c) = prod (i ↦ lift(c i)).

Русский

Подъём коммутирует с конечными произведениями: lift(prod c) = prod (i ↦ lift(c i)).

LaTeX

$$$ \operatorname{lift}(\operatorname{prod} c) = \operatorname{prod} (\lambda i. \operatorname{lift}(c(i))) $$$

Lean4

@[simp]
theorem lift_prod {ι : Type u} (c : ι → Cardinal.{v}) : lift.{w} (prod c) = prod fun i => lift.{w} (c i) :=
  by
  lift c to ι → Type v using fun _ => trivial
  simp only [← mk_pi, ← mk_uLift]
  exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

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