rename_rightInverse — Mathlib

English

If hf is a RightInverse between f and g, then rename f has a right inverse rename g.

Русский

Если hf — правый обратный к f и g, то rename f имеет правый обратный rename g.

LaTeX

$$$\\text{RightInverse}(\\text{rename}_f, \\text{rename}_g) \\quad\\text{as in the previous statement.}$$$

Lean4

theorem rename_rightInverse {f : σ → τ} {g : τ → σ} (hf : Function.RightInverse f g) :
    Function.RightInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g) :=
  rename_leftInverse hf

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