right_inv — Mathlib

English

There is a natural CoeFun instance identifying the nonlinear right inverse of a continuous linear map with its underlying function.

Русский

Существует естественный экземпляр CoeFun, который идентифицирует нелинейную правую инверсию непрерывного линейного отображения с его базовой функцией.

LaTeX

$$$$\\text{coe} : \\text{ContinuousLinearMap.NonlinearRightInverse}(f) \\to (F \\to E)$$$$

Lean4

@[simp]
theorem right_inv {f : E →SL[σ] F} (fsymm : NonlinearRightInverse f) (y : F) : f (fsymm y) = y :=
  fsymm.right_inv' y

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