We define the supremum of an arbitrary subset of seminorm 𝕜 E as follows:

• if s is bdd_above as a set of functions E → ℝ (that is, if s is pointwise bounded above), we take the pointwise supremum of all elements of s, and we prove that it is indeed a seminorm.
• otherwise, we take the zero seminorm ⊥.

There are two things worth mentionning here:

• First, it is not trivial at first that s being bounded above by a function implies being bounded above as a seminorm. We show this in seminorm.bdd_above_iff by using that the Sup s as defined here is then a bounding seminorm for s. So it is important to make the case disjunction on bdd_above (coe_fn '' s : set (E → ℝ)) and not bdd_above s.
• Since the pointwise Sup already gives 0 at points where a family of functions is not bounded above, one could hope that just using the pointwise Sup would work here, without the need for an additional case disjunction. As discussed on Zulip, this doesn't work because this can give a function which does not satisfy the seminorm axioms (typically sub-additivity).

seminorm 𝕜 E is a conditionally complete lattice.

Note that, while inf, sup and Sup have good definitional properties (corresponding to seminorm.has_inf, seminorm.has_sup and seminorm.has_Sup respectively), Inf 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 Inf 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.