instAdd — Mathlib

English

The addition of two GroupNorm structures is defined componentwise: (p + q)(x) = p(x) + q(x).

Русский

Сложение двух структур GroupNorm задаётся поэлементно: (p + q)(x) = p(x) + q(x).

LaTeX

$$$ (p+q)(x) = p(x) + q(x) $$$

Lean4

@[to_additive]
instance : Add (GroupNorm E) :=
  ⟨fun p q =>
    { p.toGroupSeminorm + q.toGroupSeminorm with
      eq_one_of_map_eq_zero' := fun _x hx =>
        of_not_not fun h => hx.not_gt <| add_pos (map_pos_of_ne_one p h) (map_pos_of_ne_one q h) }⟩

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