Skip to main content
1 of 8
wlad
  • 4.9k
  • 2
  • 21
  • 45

$f' = 0 \implies \forall x,y. f(x) = f(y)$ in choiceless constructive foundations, assuming only pointwise differentiability

Prove, without any Choice principles or Excluded Middle, that if a pointwise differentiable function has derivative $0$ everywhere, then it is constant.

The usual proof of this proposition is via the Mean Value Theorem or the Law of Bounded Change. However the former is non-constructive, and the truth of the latter (in the absence of Dependent Choice) is an open problem.

Similar questions about elementary analysis in weak foundations have been asked before on this site. For instance, see: Approximate intermediate value theorem in pure constructive mathematics

wlad
  • 4.9k
  • 2
  • 21
  • 45