equiv_symm_sub — Mathlib

English

Inverse equivalence preserves subtraction: 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_sub (since := "2025-06-08")]
theorem equiv_symm_sub [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

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