ofLeftInverse_symm_apply — Mathlib

English

If h encodes a left inverse data for f and g, then the inverse of the corresponding linear equivalence sends elements of the range of f back to their preimages via g.

Русский

Если h задаёт левый обратный для f и g, то обратное отображение соответствующего линейного эквивалента переводит элементы образа f обратно к их предобразам через g.

LaTeX

$$$(\\mathrm{ofLeftInverse}(h))^{-1}(x)=g(x) \\quad \\text{for } x \\in \\mathrm{range}(f).$$$

Lean4

@[simp]
theorem ofLeftInverse_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f)
    (x : LinearMap.range f) : (ofLeftInverse h).symm x = g x :=
  rfl

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