constant if fderiv is zero on connected open sets

Stream: Is there code for X?

[Yourong Zang]

Is there a version of convex.is_const_of_fderiv_within_eq_zero (docs#convex.is_const_of_fderiv_within_eq_zero) for connected open sets? It's easy to prove but I couldn't find one (or I did not guess its name correctly).