toNonlinearRightInverse — Mathlib

English

For fsymm : NonlinearRightInverse f, bound' yields ‖fsymm y‖ ≤ fsymm.nnnorm · ‖y‖ for all y.

Русский

Для fsymm: NonlinearRightInverse f выполняется неравенство ‖fsymm y‖ ≤ fsymm.nnnorm · ‖y‖ для всех y.

LaTeX

$$$$\\|\\text{fsymm}(y)\\| \\leq \\text{fsymm.nnnorm} \\cdot \\|y\\|.$$$$

Lean4

/-- Given a continuous linear equivalence, the inverse is in particular an instance of
`ContinuousLinearMap.NonlinearRightInverse` (which turns out to be linear). -/
noncomputable def toNonlinearRightInverse [RingHomInvPair σ' σ] (f : E ≃SL[σ] F) :
    ContinuousLinearMap.NonlinearRightInverse (f : E →SL[σ] F)
    where
  toFun := f.invFun
  nnnorm := ‖(f.symm : F →SL[σ'] E)‖₊
  bound' _ := ContinuousLinearMap.le_opNorm (f.symm : F →SL[σ'] E) _
  right_inv' := f.apply_symm_apply

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