appendFun_comp_splitFun — Mathlib

English

There is a compatibility between appendFun and splitFun: appendFun f1 g1 ∘ splitFun f0 g0 equals splitFun (f1 ∘ f0) (g1 ∘ g0).

Русский

Существует совместимость между appendFun и splitFun: appendFun f1 g1 ∘ splitFun f0 g0 = splitFun (f1 ∘ f0) (g1 ∘ g0).

LaTeX

$$$(\mathrm{appendFun}\ f1\ g1) \circ (\mathrm{splitFun}\ f0\ g0) = \mathrm{splitFun}\ (f1 \circ f0)\ (g1 \circ g0)$$$

Lean4

theorem appendFun_comp_splitFun {α γ : TypeVec n} {β δ : Type*} {ε : TypeVec (n + 1)} (f₀ : drop ε ⟹ α) (f₁ : α ⟹ γ)
    (g₀ : last ε → β) (g₁ : β → δ) :
    appendFun f₁ g₁ ⊚ splitFun f₀ g₀ = splitFun (α' := γ.append1 δ) (f₁ ⊚ f₀) (g₁ ∘ g₀) :=
  (splitFun_comp _ _ _ _).symm

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