bind₁_comp_rename — Mathlib

English

Let f : τ → MvPolynomial υ R and g : σ → τ. Then composing bind₁ with rename g is the same as bind₁ with the composed map f ∘ g.

Русский

Пусть f : τ → MvPolynomial υ R и g : σ → τ. Тогда сопоставление bind₁ с переименованием g равно bind₁ с порождаемой композицией f ∘ g.

LaTeX

$$$$ (\mathrm{bind}_1\, f) \circ (\mathrm{rename}\, g) = \mathrm{bind}_1\, (f \circ g) $$$$

Lean4

theorem bind₁_comp_rename {υ : Type*} (f : τ → MvPolynomial υ R) (g : σ → τ) :
    (bind₁ f).comp (rename g) = bind₁ (f ∘ g) := by
  ext1 i
  simp

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