instMax — Mathlib

English

There exists a maximum operation on GroupNorm E, defined by p ⊔ q with a compatibility condition ensuring the norm units.

Русский

Существует операция максимум на GroupNorm E, задаваемая p ⊔ q и совместимая с единичным элементом норм.

LaTeX

$$$\text{Max}(GroupNorm\,E)$ with $p \sqcup q$ defined componentwise$$

Lean4

@[to_additive]
instance : Max (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 <| lt_sup_iff.2 <| Or.inl <| map_pos_of_ne_one p h }⟩

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