leftInverse_of_comp — Mathlib

English

For any endomorphism f, composing with the identity yields f: f ∘ id = f and id ∘ f = f.

Русский

Для любого эндоморфизма f композиция с тождественным отображением дает f: f ∘ id = f и id ∘ f = f.

LaTeX

$$$f \\circ \\mathrm{id} = f$ and $\\mathrm{id} \\circ f = f$.$$

Lean4

/-- `g ∘ f = id` as `ContinuousLinearMap`s implies `g ∘ f = id` as functions. -/
theorem leftInverse_of_comp {f : E →L[R] F} {g : F →L[R] E} (hinv : g.comp f = ContinuousLinearMap.id R E) :
    Function.LeftInverse g f := by simpa [← Function.rightInverse_iff_comp] using congr(⇑$hinv)

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