English
The collection of seminorms on E forms a conditionally complete lattice under the pointwise order: any bounded above set has a sup and any bounded below set has an inf (where defined).
Русский
Набор семинорм на E образует условно полнотуюю решетку относительно точечного порядка: любой множество верхней границы имеет верхнюю грань, и нижнюю — нижнюю грань (где определено).
LaTeX
$$$\\text{Seminorm}_{𝕜} E \\text{ is a ConditionallyCompleteLattice under } \\le$.$$
Lean4
/-- `Seminorm 𝕜 E` is a conditionally complete lattice.
Note that, while `inf`, `sup` and `sSup` have good definitional properties (corresponding to
the instances given here for `Inf`, `Sup` and `SupSet` respectively), `sInf s` is just
defined as the supremum of the lower bounds of `s`, which is not really useful in practice. If you
need to use `sInf` on seminorms, then you should probably provide a more workable definition first,
but this is unlikely to happen so we keep the "bad" definition for now. -/
noncomputable instance instConditionallyCompleteLattice : ConditionallyCompleteLattice (Seminorm 𝕜 E) :=
conditionallyCompleteLatticeOfLatticeOfsSup (Seminorm 𝕜 E) Seminorm.isLUB_sSup
