Monotone Real Function with Everywhere Dense Image is Continuous/Lemma

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $I$ and $J$ be real intervals.

Let $f: I \to J$ be a monotone real function.

Let $f \sqbrk I$ denote the image of $I$ under $f$.

Let $f \sqbrk I$ be everywhere dense in $J$.

Let $c \in I$.


Then:

$\displaystyle \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c+ } \map f x} \cap f \sqbrk I \subseteq \set {\map f c}$


Proof

From Discontinuity of Monotonic Function is Jump Discontinuity, $\displaystyle \lim_{x \mathop \to c^-} \map f x$ and $\displaystyle \lim_{x \mathop \to c^+} \map f x$ are finite.

Since $f$ is increasing:

$\displaystyle \lim_{x \mathop \to c^-} \map f x < \lim_{x \mathop \to c^+} \map f x$

Suppose $z \in \displaystyle \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x} \cap f \sqbrk I$.

Then:

$\displaystyle \exists t \in I : \map f t \in \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x}$


Case 1 : $t < c$

Suppose that $t < c$.

\(\displaystyle t\) \(<\) \(\displaystyle c\)
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(\le\) \(\displaystyle \lim_{x \mathop \to c^-} \map f x\) Definition of Increasing Real Function
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(\notin\) \(\displaystyle \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x}\) Definition of Open Real Interval

So we may discard this case.

$\Box$


Case 2 : $t = c$

Suppose that $t = c$.

\(\displaystyle t\) \(=\) \(\displaystyle c\)
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(=\) \(\displaystyle \map f c\) Definition of Mapping
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(\in\) \(\displaystyle \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x}\) Definition of Open Real Interval

So the proposition holds in this case.

$\Box$


Case 3 : $c < t$

Suppose that $t > c$.

\(\displaystyle t\) \(>\) \(\displaystyle c\)
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(\ge\) \(\displaystyle \lim_{x \mathop \to c^+} \map f x\) Definition of Increasing Real Function
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f t\) \(\notin\) \(\displaystyle \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x}\) Definition of Open Real Interval

So we may discard this case.

$\Box$


So $\map f t = c$, by Proof by Cases.


Thus:

\(\displaystyle z\) \(=\) \(\displaystyle \map f t\) Definition of $t$
\(\displaystyle \) \(=\) \(\displaystyle c\) from above
\(\displaystyle \leadsto \ \ \) \(\displaystyle z\) \(\in\) \(\displaystyle \set {\map f c}\)


Thus:

$\displaystyle z \in \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x} \cap f \sqbrk I \implies z \in \set {\map f c}$


Hence the result, by definition of subset.

$\blacksquare$