ofLeftInverse_apply — Mathlib

English

Let f: M → M₂ be a linear map and g: M₂ → M such that g ∘ f = id_M. Then the linear equivalence constructed from this left inverse acts on M by x ↦ f(x); in particular its forward map is f.

Русский

Пусть f: M → M₂ - линейное отображение и g: M₂ → M такое, что g ∘ f = id_M. Тогда линейное эквивалентное отображение, полученное из этого левого обратного отображения, действует на M как x ↦ f(x); то есть его переходная (прямой) отображение равно f.

LaTeX

$$$(\\mathrm{ofLeftInverse}(h))(x)=f(x) \\quad \\text{для всех } x\\in M.$$$

Lean4

@[simp]
theorem ofLeftInverse_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f) (x : M) :
    ↑(ofLeftInverse h x) = f x :=
  rfl

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