rename_comp_bind₁ — Mathlib

English

Let υ be a type. For f : σ → MvPolynomial τ R and g : τ → υ, the map rename g commutes with bind₁ up to the obvious rearrangement: (rename g) ∘ (bind₁ f) = bind₁ (f ↦ rename g ∘ f).

Русский

Пусть υ — тип. Тогда переименование по g после bind₁ f равен подстановке bind₁ по функции i ↦ переименование(g, f(i)).

LaTeX

$$$$ (\mathrm{rename}\, g) \circ (\mathrm{bind}_1\, f) = \mathrm{bind}_1\, (\lambda i. \mathrm{rename}\, g \big( f(i) \big)) $$$$

Lean4

theorem rename_comp_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → υ) :
    (rename g).comp (bind₁ f) = bind₁ fun i => rename g <| f i :=
  by
  ext1 i
  simp

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