rename_bind₁ — Mathlib

English

Let υ be a type. If f : σ → MvPolynomial τ R, g : τ → υ, and φ ∈ MvPolynomial σ R, then rename g applied after bind₁ f is equal to bind₁ of the function i ↦ rename g (f i) applied to φ.

Русский

Пусть υ — тип. При f : σ → MvPolynomial τ R, g : τ → υ и φ ∈ MvPolynomial σ R переименование после bind₁ f эквивалентно bind₁ по функции i ↦ rename g (f i).

LaTeX

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

Lean4

theorem rename_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → υ) (φ : MvPolynomial σ R) :
    rename g (bind₁ f φ) = bind₁ (fun i => rename g <| f i) φ :=
  AlgHom.congr_fun (rename_comp_bind₁ f g) φ

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