rename_injective — Mathlib

English

If f is injective, then rename f is injective.

Русский

Если f инъективна, то rename f инъективна.

LaTeX

$$$\\text{If } f \\text{ is injective, then } \\text{rename}_f: \\mathrm{MvPolynomial}(\\sigma,R) \\to \\mathrm{MvPolynomial}(\\tau,R) \\text{ is injective}.$$$

Lean4

theorem rename_injective (f : σ → τ) (hf : Function.Injective f) :
    Function.Injective (rename f : MvPolynomial σ R → MvPolynomial τ R) :=
  by
  have : (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
    funext (rename_eq f)
  rw [this]
  exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)

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