avewright/proofwiki-math huggingface dataset:
Theorem: Floor Function is Not Continuous on Left at Integer

Let $f$ be the real function defined as:
:$\map f x = \floor x$
where $\floor{\, \cdot \,}$ denotes the floor function.
Let $n \in \Z$ be an integer.
Then $\map f x$ is not continuous on the left at $n$.

Proof:
From Real Number is Integer iff equals Floor:
:$\floor n = n$
By definition $\floor x$ is the unique integer such that:
:$\floor x \le x < \floor x + 1$
Consider the open real interval:
:$\II = \openint {n - 1} n$
By definition of $\floor x$ we have that:
:$\forall x \in \II: \floor x = n - 1$
That is:
:$\forall x \in \II: \floor x - n = -1$
Let $\epsilon \in \R_{>0}$.
Let $\delta \in \openint {n - 1} n$.
Then:
:$\forall x \in \II: \paren n - \delta < x < n: \size {\floor x - \paren {n - 1} } < \epsilon$
That is:
:$\ds \lim_{x \mathop \to n^-} \floor x = n - 1$
But we have that:
:$\map f n = n$
That is:
:$\ds \lim_{x \mathop \to n^-} \map f x \ne \map f n$
Hence, by definition, $\map f x$ is not continuous on the left at $n$.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers/Necessary Condition

Let $\sequence {x_n}$ be a sequence in $\R$.
Let $\sequence {x_n}$ be convergent.
Then $\sequence {x_n}$ is a Cauchy sequence.

Proof:
Let $\sequence {x_n}$ be convergent.
Let $\struct {\R, d}$ be the metric space formed from $\R$ and the usual (Euclidean) metric:
:$\map d {x_1, x_2} = \size {x_1 - x_2}$
where $\size x$ is the absolute value of $x$.
This is proven to be a metric space in Real Number Line is Metric Space.
From Convergent Sequence in Metric Space is Cauchy Sequence, we have that every convergent sequence in a metric space is a Cauchy sequence.
Hence $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers/Necessary Condition

Let $\sequence {x_n}$ be a sequence in $\R$.
Let $\sequence {x_n}$ be convergent.
Then $\sequence {x_n}$ is a Cauchy sequence.

Proof:
Let $\sequence {x_n}$ be a sequence in $\R$ that converges to the limit $l \in \R$.
Let $\epsilon > 0$. 
Then also $\dfrac \epsilon 2 > 0$.
Because $\sequence {x_n}$ converges to $l$, we have:
:$\exists N: \forall n > N: \size {x_n - l} < \dfrac \epsilon 2$
So if $m > N$ and $n > N$, then:
{{begin-eqn}}
{{eqn | l = \size {x_n - x_m}
      | r = \size {x_n - l + l - x_m}
}}
{{eqn | o = \le
      | r = \size {x_n - l} + \size {l - x_m}
      | c = Triangle Inequality
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
      | c = by choice of $N$
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Thus $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers/Sufficient Condition

Let $\sequence {x_n}$ be a sequence in $\R$.
Let $\sequence {x_n}$ be a Cauchy sequence.
Then $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
We have the result Real Number Line is Metric Space.
Hence by Convergent Subsequence of Cauchy Sequence, it is sufficient to show that $\sequence {a_n}$ has a convergent subsequence.
Since $\sequence {a_n}$ is Cauchy, by Real Cauchy Sequence is Bounded, it is also bounded.
By the Bolzano-Weierstrass Theorem, $\sequence {a_n}$ has a convergent subsequence.
Hence the result.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers/Sufficient Condition

Let $\sequence {x_n}$ be a sequence in $\R$.
Let $\sequence {x_n}$ be a Cauchy sequence.
Then $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
By Real Cauchy Sequence is Bounded, $\sequence {a_n}$ is bounded.
By the Bolzano-Weierstrass Theorem, $\sequence {a_n}$ has a convergent subsequence $\sequence {a_{n_r} }$.
Let $a_{n_r} \to l$ as $r \to \infty$.
It is to be shown that $a_n \to l$ as $n \to \infty$.
Let $\epsilon \in \R_{>0}$ be a (strictly) positive real number.
Then $\dfrac \epsilon 2 > 0$.
Hence:
:$(1): \quad \exists R \in \R: \forall r > R: \size {a_{n_r} - l} < \dfrac \epsilon 2$
We have that $\sequence {a_n}$ is a Cauchy sequence.
Hence:
:$(2): \quad \exists N \in \R: \forall m > N, n > N: \size {x_m - x_n} \le \dfrac \epsilon 2$
Let $n > N$.
Let $r \in \N$ be sufficiently large that:
:$n_r > N$
and:
:$r > R$
Then $(1)$ is satisfied, and $(2)$ is satisfied with $m = n_r$.
So:
{{begin-eqn}}
{{eqn | q = \forall n > N
      | l = \size {a_n - l}
      | r = \size {a_n - a_{n_r} + a_{n_r} - l}
      | c = 
}}
{{eqn | o = \le
      | r = \size {a_n - a_{n_r} } + \size{a_{n_r} - l}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = <
      | r = \dfrac \epsilon 2 + \dfrac \epsilon 2
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
So, given $\epsilon > 0$, we have found $n \in \R$ such that:
:$\forall n > N: \size {a_n - l} < \epsilon$
Thus:
:$x_n \to l$ as $n \to \infty$.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers/Sufficient Condition

Let $\sequence {x_n}$ be a sequence in $\R$.
Let $\sequence {x_n}$ be a Cauchy sequence.
Then $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
By Real Cauchy Sequence is Bounded, $\sequence {a_n}$ is bounded.
Thus $\sequence {a_n}$ is both bounded above and bounded below.
Let us create a monotone subsequence $\sequence {b_n}$ of $\sequence {a_n}$ using the following construction:
For each $m \in \N$, let $S_m$ denote the set of elements of $\sequence {a_n}$ from $m$ onwards:
:$S_m = \set {a_n: n \ge m}$
From Real Cauchy Sequence is Bounded, we have that $S_m$ is also bounded.
Hence, by the Continuum Property, $\sup S_m$ exists.
Let $b_m := \sup S_m$.
Because $S_{m + 1} \subseteq S_m$, it follows from Supremum of Set of Real Numbers is at least Supremum of Subset that:
:$\sup S_{m + 1} \le \sup S_m$
Thus $\sequence {b_m}$ is decreasing.
By definition of $b_m$, we also have that:
:$b_m \ge a_m$
So, as $\sequence {a_n}$ is bounded below, so is $\sequence {b_m}$.
So, by the Monotone Convergence Theorem (Real Analysis), $\sequence {b_m}$ is convergent.
Let $\sequence {b_m}$ converge to $l$.
Let $\epsilon \in \R_{>0}$ be arbitrary.
We have that $\sequence {a_n}$ is a Cauchy sequence in $\R$.
We also have from Subsequence of Real Cauchy Sequence is Cauchy that $\sequence {b_n}$ is also a Cauchy sequence in $\R$.
Then there exists:
:$N_1 \in \N$ such that $\size {a_m - a_n} < \epsilon$ for $m, n \ge N_1$
:$N_2 \in \N$ such that $\size {l - b_n} < \epsilon$ for $m \ge N_2$
Let $N = \max \set {N_1, N_2}$.
By definition of $b_N$, we have that $b_N - \epsilon$ is not an upper bound of $S_N = \set {a_n: n \ge N}$.
Thus there exists $M \ge N$ such that $a_M > b_N - \epsilon$.
We note also that $a_M \le b_N$ because $b_N$ is an upper bound for $S_N$.
Now let $n \ge N$.
We have that:
{{begin-eqn}}
{{eqn | l = \size {a_n - l}
      | r = \size {a_n - a_M + a_M - b_N + b_N - l}
      | c = 
}}
{{eqn | o = \le
      | r = \size {a_n - a_M} + \size {a_M - b_N} + \size {b_N - l}
      | c = Triangle Inequality
}}
{{eqn | o = <
      | r = 3 \epsilon
      | c = 
}}
{{end-eqn}}
Hence by Convergence by Multiple of Error Term we have that $\sequence {a_n}$ converges to $l$.
{{qed}}
Theorem: Real Number Line is Banach Space

The real number line, along with the absolute value function, forms a Banach space over $\R$.

Proof:
From Real Numbers form Vector Space  we have the real number line $\R$ is a vector space over $\R$.
That the norm axioms are satisfied by the absolute value function is proven in Absolute Value is Norm.
Then we have Real Number Line is Complete Metric Space.
Hence the result.
{{qed}}
Category:Banach Spaces
Category:Real Analysis
cflqxj1ny1viimea3qpuk23q381zlev
Theorem: Convergent Subsequence of Cauchy Sequence/Normed Vector Space

Let $\struct {X, \norm {\,\cdot\,} }$ be a normed vector space.
Let $\sequence{x_n}_{n \mathop \in \N}$ be a Cauchy sequence in $\struct {X, \norm {\,\cdot\,} }$. 
Let $x \in X$.
Then $\sequence {x_n}$ converges to $x$ {{iff}} $\sequence {x_n}$ has a subsequence that converges to $x$.

Proof:
=== Necessary Condition ===
Suppose is a Cauchy sequence$\sequence {x_n}$ which converges to $x$.
By Limit of Subsequence equals Limit of Sequence, $\sequence{x_n}$ has a subsequence of itself that converges to $x$.
{{qed|lemma}}
Theorem: Combination Theorem for Continuous Functions/Complex/Sum Rule

:$f + g$ is continuous on $S$.

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall c \in S
      | l = \lim_{x \mathop \to c} \map f z
      | r = \map f c
      | c = {{Defof|Continuous Complex Function}}
}}
{{eqn | q = \forall c \in S
      | l = \lim_{x \mathop \to c} \map g z
      | r = \map g c
      | c = {{Defof|Continuous Complex Function}}
}}
{{end-eqn}}
Let $f$ and $g$ tend to the following limits:
{{begin-eqn}}
{{eqn | l = \lim_{z \mathop \to c} \map f z
      | r = l
}}
{{eqn | l = \lim_{z \mathop \to c} \map g z
      | r = m
}}
{{end-eqn}}
From the Sum Rule for Limits of Complex Functions, we have that:
:$\ds \lim_{z \mathop \to c} \paren {\map f z + \map g z} = l + m$
So, by definition of continuous again, we have that $f + g$ is continuous on $S$.
{{qed}}
Category:Combination Theorems for Continuous Functions
trsqub4kxize28ermy98fh2f22xl9px
Theorem: Combination Theorem for Continuous Functions/Complex/Multiple Rule

:$\lambda f$ is continuous on $S$.

Proof:
By definition of continuous, we have that
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map f z = \map f c$
Let $f$ tend to the following limit:
:$\ds \lim_{z \mathop \to c} \map f z = l$
From the Multiple Rule for Limits of Complex Functions, we have that:
:$\ds \lim_{z \mathop \to c} \paren {\lambda \map f z} = \lambda l$
So, by definition of continuous again, we have that $\lambda f$ is continuous on $S$.
{{qed}}
Category:Combination Theorems for Continuous Functions
992aw8jai1qgvhtmo1lkmlqqehtwrpm
Theorem: Combination Theorem for Continuous Functions/Complex/Combined Sum Rule

:$\lambda f + \mu g$ is continuous on $S$.

Proof:
By definition of continuous, we have that
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map f z = \map f c$
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map g z = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{z \mathop \to c} \map f x = l$
:$\ds \lim_{z \mathop \to c} \map g x = m$
From the Combined Sum Rule for Limits of Complex Functions, we have that:
:$\ds \lim_{z \mathop \to c} \paren {\lambda \map f z + \mu \map g z} = \lambda l + \mu m$
So, by definition of continuous again, we have that $\lambda f + \mu g$ is continuous on $S$.
{{qed}}
Category:Combination Theorems for Continuous Functions
6a3xwpdg2pabvg4kndf4bs9by58prbk
Theorem: Combination Theorem for Continuous Functions/Complex/Product Rule

:$f g$ is continuous on $S$

Proof:
By definition of continuous:
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map f z = \map f c$
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map g z = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{z \mathop \to c} \map f z = l$
:$\ds \lim_{z \mathop \to c} \map g z = m$
From the Product Rule for Limits of Complex Functions:
:$\ds \lim_{z \mathop \to c} \paren {\map f z \map g z} = l m$
So, by definition of continuous again, we have that $f g$ is continuous on $S$.
{{qed}}
Category:Combination Theorems for Continuous Functions
bv01tqybszdyhvwuz46unjkay98vv8j
Theorem: Combination Theorem for Continuous Functions/Complex/Quotient Rule

:$\dfrac f g$ is continuous on $S \setminus \set {z \in S: \map g z = 0}$
that is, on all the points $z$ of $S$ where $\map g z \ne 0$.

Proof:
By definition of continuous:
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map f z = \map f c$
:$\forall c \in S: \ds \lim_{z \mathop \to c} \map g z = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{z \mathop \to c} \map f z = l$
:$\ds \lim_{z \mathop \to c} \map g z = m$
From the Quotient Rule for Limits of Complex Functions, we have that:
:$\ds \lim_{z \mathop \to c} \frac {\map f z} {\map g z} = \frac l m$
wherever $m \ne 0$.
So, by definition of continuous again, we have that $\dfrac f g$ is continuous on all points $z$ of $S$ where $\map g z \ne 0$.
{{qed}}
Category:Combination Theorems for Continuous Functions
o5dqb229cghgcp3upyinodnxka3gyxn
Theorem: Limit of Function by Convergent Sequences/Complex Plane

Let $f$ be a complex function defined on an open subset $S \subseteq \C$, except possibly at the point $c \in S$.
Then $\ds \lim_{x \mathop \to c} \map f z = l$ {{iff}}:
:for each sequence $\sequence {z_n}$ of points of $S$ such that $\forall n \in \N_{>0}: z_n \ne c$ and $\ds \lim_{n \mathop \to \infty} z_n = c$
it is true that:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$

Proof:
=== Necessary Condition ===
Let $\ds \lim_{z \mathop \to c} \map f z = l$.
Let $\epsilon \in \R_{>0}$.
Then by definition of the limit of a complex function:
:$\exists \delta \in \R_{>0}: \cmod {\map f z - l} < \epsilon$
provided $0 < \cmod {z - c} < \delta$.
Now suppose that $\sequence {x_n}$ is a sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: z_n \ne c$
and:
:$\ds \lim_{n \mathop \to \infty} z_n = c$
Since $\delta > 0$, from the definition of the limit of a complex function:
:$\exists N \in \R_{>0}: \forall n \in \N: n > N \implies \cmod {z_n - c} < \delta$
But:
:$\forall n \in \N_{>0}: z_n \ne c$
That means:
:$0 < \cmod {z_n - c} < \delta$
But that implies:
:$\cmod {\map f {z_n} - l} < \epsilon$
That is, given a value of $\epsilon > 0$, we have found a value of $N$ such that:
:$\forall n \in \N: n > N \implies \cmod {\map f {z_n} - l} < \epsilon$
Thus:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
{{qed|lemma}}
Theorem: Combination Theorem for Limits of Functions/Complex/Sum Rule

:$\ds \lim_{z \mathop \to c} \paren {\map f z + \map g z} = l + m$

Proof:
Let $\sequence {z_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: z_n \ne c$
:$\ds \lim_{n \mathop \to \infty} z_n = c$
By Limit of Complex Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {z_n} = m$
By the Sum Rule for Complex Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\map f {z_n} + \map g {z_n} } = l + m$
Applying Limit of Complex Function by Convergent Sequences again, we get:
:$\ds \lim_{z \mathop \to c} \paren {\map f z + \map g z} = l + m$
{{qed}}
Category:Combination Theorems for Limits of Functions
h9nsxm900y19f246q0pau1wyqtl2wgd
Theorem: Convergent Subsequence of Cauchy Sequence/Metric Space

Let $\struct {A, d}$ be a metric space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a Cauchy sequence in $A$. 
Let $x \in A$.
Then $\sequence {x_n}$ converges to $x$ {{iff}} it has a subsequence that converges to $x$.

Proof:
=== Necessary Condition ===
If $\sequence {x_n}$ converges to $x$, it trivially follows that $\sequence {x_n}$ is a subsequence of itself that converges to $x$.
{{qed|lemma}}
Theorem: Combination Theorem for Limits of Functions/Complex/Multiple Rule

:$\ds \lim_{z \mathop \to c} \lambda \map f z = \lambda l$

Proof:
Let $\sequence {z_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: z_n \ne c$
:$\ds \lim_{n \mathop \to \infty} z_n = c$
By Limit of Complex Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
By the Multiple Rule for Complex Sequences:
:$\ds \lim_{n \mathop \to \infty}\lambda \map f {z_n} = \lambda l$
Applying Limit of Complex Function by Convergent Sequences again:
:$\ds \lim_{z \mathop \to c} \lambda \map f z = \lambda l$
{{qed}}
Category:Combination Theorems for Limits of Functions
2xfre9tim4t9va0vtznyes4vox1btc3
Theorem: Combination Theorem for Limits of Functions/Complex/Combined Sum Rule

:$\ds \lim_{z \mathop \to c} \paren {\lambda \map f z + \mu \map g z} = \lambda l + \mu m$

Proof:
Let $\sequence {z_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: z_n \ne c$
:$\ds \lim_{n \mathop \to \infty} z_n = c$
By Limit of Complex Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {z_n} = m$
By the Combined Sum Rule for Complex Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\lambda \map f {z_n} + \mu \map g {z_n} } = \lambda l + \mu m$
Applying Limit of Complex Function by Convergent Sequences again, we get:
:$\ds \lim_{x \mathop \to c} \paren {\lambda \map f z + \mu \map g z} = \lambda l + \mu m$
{{qed}}
Category:Combination Theorems for Limits of Functions
kv13on64fmwt6uqd6iyhzzwf9kosg3y
Theorem: Combination Theorem for Limits of Functions/Complex/Product Rule

:$\ds \lim_{z \mathop \to c} \ \paren {\map f z \map g z} = l m$

Proof:
Let $\sequence {z_n}$ be a sequence of elements of $S$ such that:
:$\forall n \in \N: z_n \ne c$
:$\ds \lim_{n \mathop \to \infty} z_n = c$
By Limit of Complex Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {z_n} = m$
By the Product Rule for Complex Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\map f {z_n} \map g {z_n} } = l m$
Applying Limit of Complex Function by Convergent Sequences again, we get:
:$\ds \lim_{z \mathop \to c} \paren {\map f z \map g z} = l m$
{{qed}}
Category:Combination Theorems for Limits of Functions
locgfzaxckxwyq2znem5dj38twrpvz8
Theorem: Combination Theorem for Limits of Functions/Complex/Quotient Rule

:$\ds \lim_{z \mathop \to c} \frac {\map f z} {\map g z} = \frac l m$
provided that $m \ne 0$.

Proof:
Let $\sequence {z_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: z_n \ne c$
:$\ds \lim_{n \mathop \to \infty} z_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {z_n} = m$
By the Quotient Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \frac {\map f {z_n} } {\map g {z_n} } = \frac l m$
provided that $m \ne 0$.
Applying Limit of Real Function by Convergent Sequences again, we get:
:$\ds \lim_{z \mathop \to c} \frac {\map f z} {\map g z} = \frac l m$
provided that $m \ne 0$.
{{qed}}
Category:Combination Theorems for Limits of Functions
gld4cxctv6zk7t72qrd91lgjkpxb6s7
Theorem: Subset of Bounded Above Set is Bounded Above

Let $A$ and $B$ be sets of real numbers such that $A \subseteq B$.
Let $B$ be bounded above.
Then $A$ is also bounded above.

Proof:
Let $B$ be bounded above.
Then by definition $B$ has an upper bound $U$.
Hence:
:$\forall x \in B: x \le U$
But by definition of subset:
:$\forall x \in A: x \in B$
That is:
:$\forall x \in A: x \le U$
Hence, by definition, $A$ is bounded above by $U$.
{{qed}}
Theorem: Supremum of Subset of Bounded Above Set of Real Numbers

Let $A$ and $B$ be sets of real numbers such that $A \subseteq B$.
Let $B$ be bounded above.
Then:
:$\sup A \le \sup B$
where $\sup$ denotes the supremum.

Proof:
Let $B$ be bounded above.
By the Continuum Property, $B$ admits a supremum.
By Subset of Bounded Above Set is Bounded Above, $A$ is also bounded above.
Hence also by the Continuum Property, $A$ also admits a supremum.
{{AimForCont}} $\sup A > \sup B$.
Then:
:$\exists y \in A: y > \sup B$
Thus by definition of supremum, $y \notin B$.
That is:
:$A \nsubseteq B$
which contradicts our initial assumption that $A \subseteq B$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Union of Bounded Above Real Subsets is Bounded Above

Let $A$ and $B$ be sets of real numbers.
Let $A$ and $B$ be bounded above.
Then $A \cup B$ is also bounded above.

Proof:
Let $A$ and $B$ both be bounded above.
Then by definition $A$ and $B$ both have an upper bound $U_A$ and $U_B$ respectively.
Suppose $U_A \le U_B$.
Then:
:$\forall a \in A: a \le U_B$
and also, by definition:
:$\forall b \in B: b \le U_B$
and so $U_B$ is an upper bound for $A$.
Otherwise, suppose $U_A > U_B$.
Then:
:$\forall b \in B: b \le U_A$
and also, by definition:
:$\forall a \in A: a \le U_A$
Let $x \in A \cup B$.
Then from the above, either $x \le U_A$ or $x \le U_B$.
So either $U_A$ or $U_B$ is an upper bound for $A \cup B$.
Hence, by definition, $A \cup B$ is bounded above by either $U_A$ or $U_B$.
{{qed}}
Theorem: Supremum of Union of Bounded Above Sets of Real Numbers

Let $A$ and $B$ be sets of real numbers.
Let $A$ and $B$ both be bounded above.
Then:
:$\map \sup {A \cup B} = \max \set {\sup A, \sup B}$
where $\sup$ denotes the supremum.

Proof:
Let $A$ and $B$ both be bounded above.
By the Continuum Property, $A$ and $B$ both admit a supremum.
Let $x \in A \cup B$.
Then either $x \le \sup A$ or $x \le \sup B$ by definition of supremum.
Hence:
:$x \le \max \set {\sup A, \sup B}$
and so $\max \set {\sup A, \sup B}$ is certainly an upper bound of $A \cup B$.
It remains to be shown that $\max \set {\sup A, \sup B}$ is the smallest upper bound.
{{AimForCont}} there exists $m \in \R$ such that:
:$m < \max \set {\sup A, \sup B}$
and:
:$\forall x \in A \cup B: x \le m$
{{WLOG}}, let $\sup A \ge \sup B$.
Then:
:$\max \set {\sup A, \sup B} = \sup A$
and so:
:$m < \sup A$
But then by definition of supremum:
:$\exists a \in A: a > m$
and so $m$ is not an upper bound of $A \cup B$.
This contradicts our assumption that $m$ is a supremum of $A \cup B$.
It follows by Proof by Contradiction that $\max \set {\sup A, \sup B}$ is the supremum of $A \cup B$.
The same argument shows, {{mutatis}}, that if $\sup A \le \sup B$, $\max \set {\sup A, \sup B}$ is the supremum of $A \cup B$.
{{qed}}
Theorem: Subset of Bounded Below Set is Bounded Below

Let $A$ and $B$ be sets of real numbers such that $A \subseteq B$.
Let $B$ be bounded below.
Then $A$ is also bounded below.

Proof:
Let $B$ be bounded below.
Then by definition $B$ has a lower bound $L$.
Hence:
:$\forall x \in B: x \ge L$
But by definition of subset:
:$\forall x \in A: x \in B$
That is:
:$\forall x \in A: x \ge L$
Hence, by definition, $A$ is bounded below by $L$.
{{qed}}
Theorem: Infimum of Subset of Bounded Below Set of Real Numbers

Let $A$ and $B$ be sets of real numbers such that $A \subseteq B$.
Let $B$ be bounded below.
Then:
:$\inf A \ge \inf B$
where $\inf$ denotes the infimum.

Proof:
Let $B$ be bounded below.
By the Continuum Property, $B$ admits an infimum.
By Subset of Bounded Below Set is Bounded Below, $A$ is also bounded below.
Hence also by the Continuum Property, $A$ also admits a infimum.
{{AimForCont}} $\inf A < \inf B$.
Then:
:$\exists y \in A: y < \inf B$
Thus by definition of infimum, $y \notin B$.
That is:
:$A \nsubseteq B$
which contradicts our initial assumption that $A \subseteq B$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Infimum of Union of Bounded Below Sets of Real Numbers

Let $A$ and $B$ be sets of real numbers.
Let $A$ and $B$ both be bounded below.
Then:
:$\map \inf {A \cup B} = \min \set {\inf A, \inf B}$
where $\inf$ denotes the infimum.

Proof:
Let $A$ and $B$ both be bounded below.
By the Continuum Property, $A$ and $B$ both admit an infimum.
Let $x \in A \cup B$.
Then either $x \ge \inf A$ or $x \ge \inf B$ by definition of infimum.
Hence:
:$x \ge \min \set {\inf A, \inf B}$
and so $\min \set {\inf A, \inf B}$ is certainly a lower bound of $A \cup B$.
It remains to be shown that $\min \set {\inf A, \inf B}$ is the greatest lower bound.
{{AimForCont}} there exists $m \in \R$ such that:
:$m > \min \set {\inf A, \inf B}$
and:
:$\forall x \in A \cup B: x \ge m$
{{WLOG}}, let $\inf A \le \inf B$.
Then:
:$\min \set {\inf A, \inf B} = \sup A$
and so:
:$m > \sup A$
But then by definition of infimum:
:$\exists a \in A: a < m$
and so $m$ is not a lower bound of $A \cup B$.
This contradicts our assumption that $m$ is an infimum of $A \cup B$.
It follows by Proof by Contradiction that $\min \set {\inf A, \inf B}$ is the infimum of $A \cup B$.
The same argument shows, {{mutatis}}, that if $\inf A \le \inf B$, $\min \set {\inf A, \inf B}$ is the infimum of $A \cup B$.
{{qed}}