leftInvEquiv_symm_fromLeftInv — Mathlib

English

For x ∈ S.leftInv, the inverse symm of leftInvEquiv applied to fromLeftInv x yields x, i.e., (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x.

Русский

Для x ∈ S.leftInv, обратная часть эквивалентности восстанавливает x: (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x.

LaTeX

$$$ (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x $$$

Lean4

@[to_additive (attr := simp)]
theorem leftInvEquiv_symm_fromLeftInv (x : S.leftInv) : (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x :=
  (S.leftInvEquiv hS).left_inv x

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