equiv_equivWithAbs_symm_apply — Mathlib

English

For any v, w and x in WithAbs w, equiv v((equivWithAbs v w)^{-1}(x)) = equiv w (x)^{-1}.

Русский

Для любых v, w и x в WithAbs w выполняется равенство: equiv v((equivWithAbs v w)^{-1}(x)) = equiv w (x).

LaTeX

$$equiv(v)\\big((equivWithAbs(v,w))^{-1}(x)\\big) = (equiv(w))^{-1}(x)$$

Lean4

@[simp]
theorem equiv_equivWithAbs_symm_apply {v w : AbsoluteValue R S} {x : WithAbs w} :
    equiv v ((equivWithAbs v w).symm x) = equiv w x :=
  rfl

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