WithLp.equiv_symm_sub

theorem WithLp.equiv_symm_sub : ∀ (p : ENNReal) {V : Type uV} [inst : AddCommGroup V] (x' y' : V), (WithLp.equiv p V).symm (x' - y') = (WithLp.equiv p V).symm x' - (WithLp.equiv p V).symm y'

This theorem states that for any extended nonnegative real number `p`, for any type `V` that is an additive commutative group, and for any two elements `x'` and `y'` of type `V`, the difference `x' - y'` under the inverse of the canonical equivalence `WithLp.equiv` between `WithLp p V` and `V` is equal to the difference between `x'` under the inverse equivalence and `y'` under the inverse equivalence. In other words, the inverse equivalence preserves the subtraction operation.

More concisely: For any extended nonnegative real number `p`, any additive commutative group `V`, and any `x, y` in `V`, the inverse of the canonical equivalence between `WithLp p V` and `V` preserves the subtraction operation, that is, `WithLp.equiv.symm (x' - y') = x' - WithLp.equiv.symm y'` in `V`.