appendFun_comp' — Mathlib

English

Another variant of the distributivity: (f1 ::: g1) ∘ (f0 ::: g0) equals (f1 ∘ f0 ::: g1 ∘ g0).

Русский

Другая форма распределения: (f1 ::: g1) ∘ (f0 ::: g0) = (f1 ∘ f0 ::: g1 ∘ g0).

LaTeX

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

Lean4

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

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