append_prod_appendFun — Mathlib

English

The composition of appendFun with prod.map equals the prod.map of appendFun applied componentwise

Русский

Компоновка appendFun с prod.map равна prod.map от appendFun применённому по компонентам

LaTeX

$$\operatorname{appendFun} (\operatorname{prod.map} f_0 g_0) (\operatorname{Prod.map} f_1 g_1) = \operatorname{Prod.map} (\operatorname{appendFun} f_0 f_1) (\operatorname{appendFun} g_0 g_1)$$

Lean4

theorem append_prod_appendFun {n} {α α' β β' : TypeVec.{u} n} {φ φ' ψ ψ' : Type u} {f₀ : α ⟹ α'} {g₀ : β ⟹ β'}
    {f₁ : φ → φ'} {g₁ : ψ → ψ'} : ((f₀ ⊗' g₀) ::: (_root_.Prod.map f₁ g₁)) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) :=
  by
  ext i a
  cases i
  · cases a
    rfl
  · rfl

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