instAdd — Mathlib

English

There is a natural addition operation on GroupSeminorm E: (p + q)(x) = p(x) + q(x).

Русский

Существует естественное сложение на GroupSeminorm E: (p + q)(x) = p(x) + q(x).

LaTeX

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

Lean4

@[to_additive]
instance : Add (GroupSeminorm E) :=
  ⟨fun p q =>
    { toFun := fun x => p x + q x
      map_one' := by simp_rw [map_one_eq_zero p, map_one_eq_zero q, zero_add]
      mul_le' := fun _ _ =>
        (add_le_add (map_mul_le_add p _ _) <| map_mul_le_add q _ _).trans_eq <| add_add_add_comm _ _ _ _
      inv' := fun x => by simp_rw [map_inv_eq_map p, map_inv_eq_map q] }⟩

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