Pointwise operations on ordered algebraic objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.