linearEquivOfLeftInverse_apply — Mathlib

English

If f is left inverse of g, then the constructed linear equivalence sends x to f(x).

Русский

Если f является левым обратным к g, то соответствующее линейное эквивалентное отображение отправляет x в f(x).

LaTeX

$$linearEquivOfLeftInverse hfg x = f x$$

Lean4

@[simp]
theorem linearEquivOfLeftInverse_apply (hfg : Function.LeftInverse f g) (x : M) :
    linearEquivOfLeftInverse hfg x = f x :=
  rfl

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