ofLeftInverse_symm_apply — Mathlib

English

The inverse of the left-inverse-based equivalence, when applied to an element of f.range, gives g(x).

Русский

Обратное к эквиваленции, построенной по левому обратному, при применении к элементу образа f равняется g(x).

LaTeX

$$$$ (\\mathrm{ofLeftInverse}(h))^{-1}(x) = g(x) $$$$

Lean4

@[to_additive (attr := simp)]
theorem ofLeftInverse_symm_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : f.range) :
    (ofLeftInverse h).symm x = g x :=
  rfl

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