What is the correct formulation of Rolle's Theorem

100 Views Asked by At

Generally Rolle's theorem is expressed with words. But how should it look in a formal mathematical/logic language?

$$\forall f \Big( \big(f \textrm{continue [a,b]} \land f \textrm{differentiable ]a,b[} \land f(a)=f(b) \big) \rightarrow \exists c \in ]a,b[\textrm{ s.t. }f'(c)=0 \Big)$$

$$\forall f \Big( (f \textrm{continue [a,b]} \land f \textrm{differentiable ]a,b[ }) ( f(a)=f(b) \rightarrow \exists c \in ]a,b[\textrm{ s.t. }f'(c)=0) \Big)$$

So where should we place $f(a)=f(b)$ ?

1

There are 1 best solutions below

0
On BEST ANSWER

The two formulations are logically equivalent. Indeed, $(A \land B) \to C$ is logically equivalent to $A \to (B \to C)$ (you can check it by yourself by truth table). This equivalence is called currying in several contexts of mathematics and theoretical computer science.

Note that, to be more precise, the correct formalization of the second sentence is \begin{equation} \forall f \, \big( (f \text{ cont. }[a,b] \land f \text{ diff. } ]a,b[) \to (f(a) = f(b) \to \exists c (c \in {]a,b[} \land f'(c) = 0)) \big) \end{equation} (notice the nested implications).