fromLeftInv_leftInvEquiv_symm — Mathlib

English

For any x ∈ S.leftInv, applying the leftInvEquiv and then its inverse recovers x, i.e., S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x.

Русский

Для любого x ∈ S.leftInv применение эквивалентности слева и её обратного возвращает исходное x: S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem fromLeftInv_leftInvEquiv_symm (x : S) : S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x :=
  (S.leftInvEquiv hS).right_inv x

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