equiv_add — Mathlib

English

Equivalence preserves addition: equivalence of x+y equals sum of equivalences.

Русский

Эквивалентность сохраняет сложение: эквивалентность x+y равна сумме эквивалентностей.

LaTeX

$$$WithLp.equiv p V (x + y) = WithLp.equiv p V x + WithLp.equiv p V y$$$

Lean4

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

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