semilatticeSup — Mathlib

English

The collection of GroupSeminorms on E forms a semilattice under pointwise order, with the supremum operation given by (p ⊔ q)(x) = p(x) ⊔ q(x).

Русский

Множество GroupSeminorm на E образует полупретяжку под покомпонентным порядком; верхняя граница определяется как (p ⊔ q)(x) = p(x) ⊔ q(x).

LaTeX

$$$\text{GroupSeminorm}(E) \text{ is a Semilattice under pointwise order with } (p \sqcup q)(x) = p(x) \sqcup q(x).$$$

Lean4

@[to_additive]
instance semilatticeSup : SemilatticeSup (GroupSeminorm E) :=
  DFunLike.coe_injective.semilatticeSup _ coe_sup

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