coe_apply_coe_coe_symm_apply — Mathlib

English

Applying an equivalence and then the inverse mapping recovers the original element.

Русский

Применение эквивалентности и затем обратного отображения восстанавливает исходный элемент.

LaTeX

$$$ f((f^{-1}(x))) = x $ for all x$$

Lean4

@[simp]
theorem coe_apply_coe_coe_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) :
    f ((f : A₁ ≃ₐ[R] A₂).symm x) = x :=
  EquivLike.right_inv f x

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