equivWithAbs_symm_equiv_symm_apply

Mathlib.Analysis.Normed.Ring.WithAbs

URI: https://scilib.ai/kg/mathlib#WithAbs.equivWithAbs_symm_equiv_symm_apply

← MathLib Explorer

English

For x in R, (equivWithAbs v w).symm ((equiv w).symm x) = (equiv v).symm x.

Русский

Для любого x выполняется: (equivWithAbs v w).symm ((equiv w).symm x) = (equiv v).symm x.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru