Skip to main content
deleted 3 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

For the record, I provide here a proof of the constancy principle from the principle of open induction. Recall:

Principle of open induction: Let $U \subseteq [0,1]$ be an open set such that $$\forall x \in [0,1] . (\forall y \in [0,1] . y < x \Rightarrow y \in U)) \Rightarrow x \in U.$$ Then $U = [0,1]$.

We also have:

Constancy principle: For a pointwise differentiable map $f : \mathbb{R} \to \mathbb{R}$, if $f'(x) = 0$ for all $x \in \mathbb{R}$, then $f$ is constant.

Theorem: The principle of open induction implies the constancy principle.

Proof. Let $f : \mathbb{R} \to \mathbb{R}$ be pointwise differentiable with $f'(x) = 0$ for all $x \in \mathbb{R}$. Observe that $f$ is pointwise continuous. We show that $f$ is constant on $[0,1]$, and leave the generalization to arbitrary intervals as exercise.

It suffices to show that for all $\epsilon > 0$ and $x \in [0,1]$ we have $|f(x) - f(0)| < \epsilon \cdot x$. The set $$U = \{x \in [0,1] \mid |f(x) - f(0)| < \epsilon \cdot x\}, $$ is an open because $f$ is pointwise continuous. We prove that $U = [0,1]$ by open induction. Let $x \in [0,1]$ and assume that $|f(y) - f(0)| < \epsilon \cdot y$ for all $y$ such that $0 \leq y < x$. Because $f'(x) = 0$, there exists $\delta > 0$ such that $|f(x) - f(z)| < \epsilon \cdot (x - z)$ for all $z$ such that $x - \delta < z < x$. We have $x < \delta$ or $x > \delta/2$:

  1. If $x < \delta$ then we take $z = 0$ to directly obtain the desired inequality $|f(x) - f(0)| < \epsilon \cdot x$.

  2. If $x > \delta/2$ then we take $z = x - \delta/4$, so that $|f(z) - f(0)| < \epsilon \cdot z$ by assumption, and conclude by \begin{align*} |f(x) - f(0) &\leq |f(x) - f(z)| + |f(z) - f(0)| \\ &< \epsilon \cdot (x - z) + \epsilon \cdot z \\ &= \epsilon \cdot x. \end{align*}

For the record, I provide here a proof of the constancy principle from the principle of open induction. Recall:

Principle of open induction: Let $U \subseteq [0,1]$ be an open set such that $$\forall x \in [0,1] . (\forall y \in [0,1] . y < x \Rightarrow y \in U)) \Rightarrow x \in U.$$ Then $U = [0,1]$.

We also have:

Constancy principle: For a pointwise differentiable map $f : \mathbb{R} \to \mathbb{R}$, if $f'(x) = 0$ for all $x \in \mathbb{R}$, then $f$ is constant.

Theorem: The principle of open induction implies the constancy principle.

Proof. Let $f : \mathbb{R} \to \mathbb{R}$ be pointwise differentiable with $f'(x) = 0$ for all $x \in \mathbb{R}$. Observe that $f$ is pointwise continuous. We show that $f$ is constant on $[0,1]$, and leave the generalization to arbitrary intervals as exercise.

It suffices to show that for all $\epsilon > 0$ and $x \in [0,1]$ we have $|f(x) - f(0)| < \epsilon \cdot x$. The set $$U = \{x \in [0,1] \mid |f(x) - f(0)| < \epsilon \cdot x\}, $$ is an open because $f$ is pointwise continuous. We prove that $U = [0,1]$ by open induction. Let $x \in [0,1]$ and assume that $|f(y) - f(0)| < \epsilon \cdot y$ for all $y$ such that $0 \leq y < x$. Because $f'(x) = 0$, there exists $\delta > 0$ such that $|f(x) - f(z)| < \epsilon \cdot (x - z)$ for all $z$ such that $x - \delta < z < x$. We have $x < \delta$ or $x > \delta/2$:

  1. If $x < \delta$ then we take $z = 0$ to directly obtain the desired inequality $|f(x) - f(0)| < \epsilon \cdot x$.

  2. If $x > \delta/2$ then we take $z = x - \delta/4$, so that $|f(z) - f(0)| < \epsilon \cdot z$ by assumption, and conclude by \begin{align*} |f(x) - f(0) &\leq |f(x) - f(z)| + |f(z) - f(0)| \\ &< \epsilon \cdot (x - z) + \epsilon \cdot z \\ &= \epsilon \cdot x. \end{align*}

For the record, I provide here a proof of the constancy principle from the principle of open induction. Recall:

Principle of open induction: Let $U \subseteq [0,1]$ be an open set such that $$\forall x \in [0,1] . (\forall y \in [0,1] . y < x \Rightarrow y \in U)) \Rightarrow x \in U.$$ Then $U = [0,1]$.

We also have:

Constancy principle: For a pointwise differentiable map $f : \mathbb{R} \to \mathbb{R}$, if $f'(x) = 0$ for all $x \in \mathbb{R}$, then $f$ is constant.

Theorem: The principle of open induction implies the constancy principle.

Proof. Let $f : \mathbb{R} \to \mathbb{R}$ be pointwise differentiable with $f'(x) = 0$ for all $x \in \mathbb{R}$. Observe that $f$ is pointwise continuous. We show that $f$ is constant on $[0,1]$, and leave the generalization to arbitrary intervals as exercise.

It suffices to show that for all $\epsilon > 0$ and $x \in [0,1]$ we have $|f(x) - f(0)| < \epsilon \cdot x$. The set $$U = \{x \in [0,1] \mid |f(x) - f(0)| < \epsilon \cdot x\}, $$ is open because $f$ is pointwise continuous. We prove that $U = [0,1]$ by open induction. Let $x \in [0,1]$ and assume that $|f(y) - f(0)| < \epsilon \cdot y$ for all $y$ such that $0 \leq y < x$. Because $f'(x) = 0$, there exists $\delta > 0$ such that $|f(x) - f(z)| < \epsilon \cdot (x - z)$ for all $z$ such that $x - \delta < z < x$. We have $x < \delta$ or $x > \delta/2$:

  1. If $x < \delta$ then we take $z = 0$ to directly obtain the desired inequality $|f(x) - f(0)| < \epsilon \cdot x$.

  2. If $x > \delta/2$ then we take $z = x - \delta/4$, so that $|f(z) - f(0)| < \epsilon \cdot z$ by assumption, and conclude by \begin{align*} |f(x) - f(0) &\leq |f(x) - f(z)| + |f(z) - f(0)| \\ &< \epsilon \cdot (x - z) + \epsilon \cdot z \\ &= \epsilon \cdot x. \end{align*}

Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

For the record, I provide here a proof of the constancy principle from the principle of open induction. Recall:

Principle of open induction: Let $U \subseteq [0,1]$ be an open set such that $$\forall x \in [0,1] . (\forall y \in [0,1] . y < x \Rightarrow y \in U)) \Rightarrow x \in U.$$ Then $U = [0,1]$.

We also have:

Constancy principle: For a pointwise differentiable map $f : \mathbb{R} \to \mathbb{R}$, if $f'(x) = 0$ for all $x \in \mathbb{R}$, then $f$ is constant.

Theorem: The principle of open induction implies the constancy principle.

Proof. Let $f : \mathbb{R} \to \mathbb{R}$ be pointwise differentiable with $f'(x) = 0$ for all $x \in \mathbb{R}$. Observe that $f$ is pointwise continuous. We show that $f$ is constant on $[0,1]$, and leave the generalization to arbitrary intervals as exercise.

It suffices to show that for all $\epsilon > 0$ and $x \in [0,1]$ we have $|f(x) - f(0)| < \epsilon \cdot x$. The set $$U = \{x \in [0,1] \mid |f(x) - f(0)| < \epsilon \cdot x\}, $$ is an open because $f$ is pointwise continuous. We prove that $U = [0,1]$ by open induction. Let $x \in [0,1]$ and assume that $|f(y) - f(0)| < \epsilon \cdot y$ for all $y$ such that $0 \leq y < x$. Because $f'(x) = 0$, there exists $\delta > 0$ such that $|f(x) - f(z)| < \epsilon \cdot (x - z)$ for all $z$ such that $x - \delta < z < x$. We have $x < \delta$ or $x > \delta/2$:

  1. If $x < \delta$ then we take $z = 0$ to directly obtain the desired inequality $|f(x) - f(0)| < \epsilon \cdot x$.

  2. If $x > \delta/2$ then we take $z = x - \delta/4$, so that $|f(z) - f(0)| < \epsilon \cdot z$ by assumption, and conclude by \begin{align*} |f(x) - f(0) &\leq |f(x) - f(z)| + |f(z) - f(0)| \\ &< \epsilon \cdot (x - z) + \epsilon \cdot z \\ &= \epsilon \cdot x. \end{align*}