dropFun_comp — Mathlib

English

DropFun preserves composition: dropFun (f1 ∘ f0) = dropFun f1 ∘ dropFun f0.

Русский

DropFun сохраняет композицию: dropFun (f1 ∘ f0) = dropFun f1 ∘ dropFun f0.

LaTeX

$$$\mathrm{dropFun}(\mathrm{f}_{1} \circ \mathrm{f}_{0}) = \mathrm{dropFun}(\mathrm{f}_{1}) \circ \mathrm{dropFun}(\mathrm{f}_{0})$$$

Lean4

@[simp]
theorem dropFun_comp {α₀ α₁ α₂ : TypeVec (n + 1)} (f₀ : α₀ ⟹ α₁) (f₁ : α₁ ⟹ α₂) :
    dropFun (f₁ ⊚ f₀) = dropFun f₁ ⊚ dropFun f₀ :=
  rfl

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