theorem SetValuedOperator.neg_chebyshevCenterActiveSet_isMonotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : Set H) : (-Φ[C]).IsMonotone

Example 20.13: the negation of the chapter's active farthest-point operator Φ[C] is monotone.