Pointwise operations on ordered algebraic objects #
This file contains lemmas about the effect of pointwise operations on sets with an order structure.
Sup (s • t) = Sup s • Sup t and
Inf (s • t) = Inf s • Inf t hold as well but
covariant_class is currently not polymorphic enough to state it.