appendFun_comp — Mathlib

English

Composition distributes over append of arrows: (f1 ∘ f0 ::: g1 ∘ g0) equals (f1 ::: g1) ∘ (f0 ::: g0).

Русский

Композиция распределяется через конкатенацию стрел: (f1 ∘ f0 ::: g1 ∘ g0) = (f1 ::: g1) ∘ (f0 ::: g0).

LaTeX

$$$ (f1 \circ f0 ::: g1 \circ g0) = (f1 ::: g1) \circ (f0 ::: g0) $$$

Lean4

theorem appendFun_comp {α₀ α₁ α₂ : TypeVec n} {β₀ β₁ β₂ : Type*} (f₀ : α₀ ⟹ α₁) (f₁ : α₁ ⟹ α₂) (g₀ : β₀ → β₁)
    (g₁ : β₁ → β₂) : (f₁ ⊚ f₀ ::: g₁ ∘ g₀) = (f₁ ::: g₁) ⊚ (f₀ ::: g₀) :=
  eq_of_drop_last_eq rfl rfl

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