equiv_symm_add — Mathlib

English

Inverse equivalence preserves addition: symm(x'+y') = symm x' + symm y'.

Русский

Обратная эквивалентность сохраняет сложение: symm(x'+y') = symm x' + symm y'.

LaTeX

$$$(WithLp.equiv p V).\text{symm} (x' + y') = (WithLp.equiv p V).\text{symm} x' + (WithLp.equiv p V).\text{symm} y'$$$

Lean4

@[deprecated toLp_add (since := "2025-06-08")]
theorem equiv_symm_add [AddCommGroup V] (x' y' : V) :
    (WithLp.equiv p V).symm (x' + y') = (WithLp.equiv p V).symm x' + (WithLp.equiv p V).symm y' :=
  rfl

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