English
There is a Max (sup) operation on GroupSeminorm E defined pointwise by (p ⊔ q)(x) = max(p(x), q(x)).
Русский
Существуют операции максимума (sup) на GroupSeminorm E, заданные точечно: (p ⊔ q)(x) = max(p(x), q(x)).
LaTeX
$$(p ⊔ q)(x) = \\max\\{ p(x), q(x) \\}$$
Lean4
@[to_additive]
instance : Max (GroupSeminorm E) :=
⟨fun p q =>
{ toFun := p ⊔ q
map_one' := by rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]
mul_le' := fun x y =>
sup_le ((map_mul_le_add p x y).trans <| add_le_add le_sup_left le_sup_left)
((map_mul_le_add q x y).trans <| add_le_add le_sup_right le_sup_right)
inv' := fun x => by rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, map_inv_eq_map q] }⟩
