lastFun_prod — Mathlib

English

The lastFun of a product map equals the product map of the lastFuns.

Русский

Последняя функция произведения равна произведению последних функций.

LaTeX

$$\operatorname{lastFun}(f \otimes' f') = \operatorname{Prod.map}(\operatorname{lastFun} f)(\operatorname{lastFun} f')$$

Lean4

@[simp]
theorem lastFun_prod {α α' β β' : TypeVec (n + 1)} (f : α ⟹ β) (f' : α' ⟹ β') :
    lastFun (f ⊗' f') = Prod.map (lastFun f) (lastFun f') :=
  rfl

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