rightInverse_of_comp — Mathlib

English

For a finite set s and a family of endomorphisms g i, the sum over i in s of g i comp f equals the sum of compositions: (∑_{i∈s} g i) ∘ f = ∑_{i∈s} (g i ∘ f).

Русский

Для конечного множества s и семейства эндоморфизмов g_i выполняется (∑ g_i) ∘ f = ∑ (g_i ∘ f).

LaTeX

$$$\\left(\\sum_{i\\in s} g_i\\right) \\circ f = \\sum_{i\\in s} (g_i \\circ f).$$$

Lean4

/-- `f ∘ g = id` as `ContinuousLinearMap`s implies `f ∘ g = id` as functions. -/
theorem rightInverse_of_comp {f : E →L[R] F} {g : F →L[R] E} (hinv : f.comp g = ContinuousLinearMap.id R F) :
    Function.RightInverse g f :=
  leftInverse_of_comp hinv

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