avewright/proofwiki-math huggingface dataset:
Theorem: Approximation to Binary Logarithm from Natural and Common Logarithm

The binary logarithm $\lg x$ can be approximated, to within $1 \%$, by the expression:
:$\lg x \approx \ln x + \log_{10} x$
That is, by the sum of the natural logarithm and common logarithm.

Proof:
{{begin-eqn}}
{{eqn | l = \lg x 
      | r = \frac {\ln x} {\ln 2}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\log_{10} x} {\log_{10} 2}
      | c = Change of Base of Logarithm
}}
{{eqn | ll= \leadsto
      | l = \lg x
      | r = \frac {\ln x + \log_{10} x} {\ln 2 + \log_{10} 2}
      | c = 
}}
{{eqn | r = \frac {\ln x + \log_{10} x} {\ln 2 + \frac {\ln 2} {\ln 10} }
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\ln x + \log_{10} x} {\ln 2 \left({1 + \frac 1 {\ln 10} }\right)}
      | c = 
}}
{{eqn | r = \frac {\ln x + \log_{10} x} {\ln 2 \left({1 + \log_{10} e}\right)}
      | c = Reciprocal of Logarithm
}}
{{end-eqn}}
We have that:
:$\ln 2 = 0 \cdotp 69347 \ 1805 \ldots$
:$\log_{10} e = 0 \cdotp 43429 \ 44819 \ldots$
Thus:
{{begin-eqn}}
{{eqn | l = \ln 2 \left({1 + \log_{10} e}\right)
      | r = 0 \cdotp 69347 \ 1805 \ldots \left({1 + 0 \cdotp 43429 \ 44819 \ldots}\right)
      | c = 
}}
{{eqn | r = 0 \cdotp 99462 \ldots
      | c = 
}}
{{end-eqn}}
Hence:
:$\lg x + \log_{10} x \approx 0 \cdotp 994 \ln x$
That is, the approximation is $99.4 \%$ accurate.
{{qed}}
Theorem: Value of b for b by Logarithm Base b of x to be Minimum

Let $x \in \R_{> 0}$ be a (strictly) positive real number.
Consider the real function $f: \R_{> 0} \to \R$ defined as:
:$\map f b := b \log_b x$
$f$ attains a minimum when
:$b = e$
where $e$ is Euler's number.

Proof:
From the Interior Extremum Theorem, when $f$ is at a minimum, its derivative $\dfrac \d {\d b} f$ will be zero.
Let $y = \map f b$.
We have:
{{begin-eqn}}
{{eqn | l = y
      | r = b \log_b x
      | c = 
}}
{{eqn | r = \frac {b \ln x} {\ln b} 
      | c = Change of Base of Logarithm
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d b}
      | r = \frac {\ln b \frac \d {\d b} \paren {b \ln x} - b \ln x \frac \d {\d b} \ln b} {\paren {\ln b}^2}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \frac {\ln b \ln x - b \ln x \frac 1 b} {\paren {\ln b}^2}
      | c = Derivative of Natural Logarithm, Derivative of Identity Function
}}
{{eqn | r = \frac {\ln x} {\ln b} \paren {1 - \frac 1 {\ln b} }
      | c = simplifying
}}
{{eqn | r = \frac {\ln x} {\ln b^2} \paren {\ln b - 1}
      | c = simplifying
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d b} 
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\ln x} {\ln b}
      | r = \frac {\ln x} {\paren {\ln b}^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ln b
      | r = 1
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = b
      | r = e
      | c = {{Defof|Natural Logarithm}}
}}
{{end-eqn}}
To determine that $f$ is a minimum at this point, we differentiate again {{WRT|Differentiation}} $b$:
{{begin-eqn}}
{{eqn | l = \frac {\d^2 y} {\d b^2}
      | r = \map {\frac \d {\d b} } {\frac {\ln x} {\ln b^2} \paren {\ln b - 1} }
      | c = 
}}
{{eqn | r = \frac {\ln x} b \paren {\frac {\ln b - 2 \paren {\ln b - 1} } {\paren {\ln b}^3} }
      | c = 
}}
{{end-eqn}}
Setting $b = e$ gives:
:$\valueat {\dfrac {\d^2 y} {\d b^2} } {b \mathop = e} = \dfrac {\ln x} e \dfrac {\paren {1 - 2 \paren 0} } 1$
which works out to be (strictly) positive.
From Real Function with Strictly Positive Second Derivative is Strictly Convex, $f$ is strictly convex at this point.
Thus $f$ is a minimum.
{{qed}}
Theorem: Monotone Real Function with Everywhere Dense Image is Continuous

Let $I$ and $J$ be real intervals.
Let $f: I \to J$ be a monotone real function.
Let $f \sqbrk I$ be everywhere dense in $J$, where $f \sqbrk I$ denotes the image of $I$ under $f$.
Then $f$ is continuous on $I$.

Proof:
{{WLOG}}, let $f$ be increasing.
{{AimForCont}} $f$ is discontinuous at $c \in I$.
Let:
:$L^-$ denote $\ds \lim_{x \mathop \to c^-} \map f x$
:$L$ denote $\map f c$
:$L^+$ denote $\ds \lim_{x \mathop \to c^+} \map f x$
From Discontinuity of Monotonic Function is Jump Discontinuity, $L^-$ and $L^+$ are (finite) real numbers.
From {{Corollary|Limit of Monotone Real Function/Increasing|disp = Limit of Monotone Real Function}}:
:$L^- \le L \le L^+$
Let $S = \openint {L^-} {L^+}$.
If $L^- = L = L^+$, then $c$ is not a discontinuity, a contradiction.
Thus $S$ is non-degenerate.
From Non-Degenerate Real Interval is Infinite, $S$ is infinite.
From Relative Difference between Infinite Set and Finite Set is Infinite, $S \setminus \set L$ is  non-empty.
From Finite Subset of Metric Space is Closed, $\set L$ is closed.
From Open Set minus Closed Set is Open, $S \setminus \set L$ is open.
Theorem: Relative Difference between Infinite Set and Finite Set is Infinite

Let $S$ be an infinite set.
Let $T$ be a finite set.
Then $S \setminus T$ is an infinite set.

Proof:
{{AimForCont}} $S \setminus T$ is a finite set.
Then:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = S \cup T
      | c = Set is Subset of Union
}}
{{eqn | r = \paren {S \setminus T} \cup T
      | c = Set Difference Union Second Set is Union
}}
{{end-eqn}}
By Union of Finite Sets is Finite, $S \cup T$ is a finite set.
By Subset of Finite Set is Finite, $S$ must also be a finite set.
But $S$ is an infinite set.
This is a contradiction.
Therefore $S \setminus T$ is an infinite set.
{{qed}}
Category:Set Difference
Category:Infinite Sets
ktntts6ukzwzcluwrgimxns9p2ils5a
Theorem: Set Difference over Subset

Let $A$, $B$, and $S$ be sets.
Let $A \subseteq B$.
Then:
:$A \setminus S \subseteq B \setminus S$

Proof:
{{begin-eqn}}
{{eqn | l = A \setminus S
      | r = A \cap \map \complement S
      | c = Set Difference as Intersection with Complement
}}
{{eqn | o = \subseteq
      | r = B \cap \map \complement S
      | c = {{Corollary|Set Intersection Preserves Subsets}}
}}
{{eqn | r = B \setminus S
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
4atyey826ay44n4dwhe3cw7f9wuww40
Theorem: Subset of Empty Set iff Empty

Let $S$ be a set.
Let $\O$ denote the empty set.
Then $S \subseteq \O$ {{iff}} $S = \O$.

Proof:
Suppose $x \in S$.
Then since $S \subseteq \O$, it follows that $x \in \O$.
Hence $x \notin S$.
That is, $S = \O$.
{{qed}}
Category:Empty Set
h7lpbqjhov78wp3cpmrvdho7zc9riec
Theorem: Finite Subset of Metric Space is Closed

Let $M = \struct {A, d}$ be a metric space.
Let $S \subseteq A$ be finite.
Then $S$ is closed in $M$.

Proof:
From Metric Space is Hausdorff, $M$ is Hausdorff.
From Finite Subspace of Hausdorff Space is Closed, $S$ is closed.
{{qed}}
Category:Closed Sets
Category:Metric Spaces
o2ifexi1cunsg6pq68v9xoyi184umf8
Theorem: Monotone Real Function with Everywhere Dense Image is Continuous/Lemma

:$\ds \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, $\ds \lim_{x \mathop \to c^-} \map f x$ and $\ds \lim_{x \mathop \to c^+} \map f x$ are finite.
Since $f$ is increasing:
:$\ds \lim_{x \mathop \to c^-} \map f x < \lim_{x \mathop \to c^+} \map f x$
Suppose $z \in \ds \openint {\lim_{x \mathop \to c^-} \map f x} {\lim_{x \mathop \to c^+} \map f x} \cap f \sqbrk I$.
Then:
:$\ds \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}$
Theorem: Defining Sequence of Natural Logarithm is Uniformly Convergent on Compact Sets

Let $x \in \R$ be a real number such that $x > 0$.
Let $\sequence {f_n}$ be the sequence of mappings $f_n : \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1}$
Let $K \subseteq \R_{>0}$ be compact.
Then $\sequence {f_n}$ is uniformly convergent on $K$.

Proof:
From Continuity of Root Function and Combination Theorem for Continuous Real Functions:
:$\forall n \in \N : \map {f_n} x$ is continuous on $K$
From Defining Sequence of Natural Logarithm is Convergent, $\sequence {f_n}$ is pointwise convergent to $\ln$.
From Real Natural Logarithm Function is Continuous, $\ln$ is continuous on $K$.
From Defining Sequence of Natural Logarithm is Strictly Decreasing:
:$\forall x \in K: \sequence {\map {f_n} x}$ is monotone.
From Dini's Theorem, $\sequence {f_n}$ is uniformly convergent to $\ln$.
Hence the result.
{{qed}}
Category:Natural Logarithms
ng8rt6v5o47l7q1ofhf7eaiieg8qqt4
Theorem: Multiplication of Positive Number by Real Number Greater than One

Let $x$ and $y$ be real numbers.
Let $x > 1$.
Let $y > 0$.
Then $\dfrac y x < y$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 1
}}
{{eqn | ll= \leadsto
      | l = \frac 1 x
      | o = <
      | r = 1
      | c = Ordering of Reciprocals
}}
{{eqn | ll= \leadsto
      | l = \frac y x
      | o = <
      | r = y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{end-eqn}}
{{qed}}
Category:Real Multiplication
Category:Inequalities
aylhlcergqss4bgexgl50e85n07nkrf
Theorem: Set of Finite Suprema is Directed

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $X$ be a non-empty subset of $S$.
Then
:$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.

Proof:
By Existence of Non-Empty Finite Suprema in Join Semilattice:
:for every $A \in \map {\operatorname {Fin} } S$ if $A \ne \O$, then $A$ admits a supremum.
By definition of non-empty set:
:$\exists a: a \in X$
By definitions of subset and singleton:
:$\set x \subseteq X$
By Singleton is Finite:
:$\set x$ is finite
By definitions of non-empty set and singleton:
:$\set x \ne \O$
By definition of $\operatorname {Fin}$:
:$\sup {\set x} \in \set {\sup A: A \in \map {\operatorname{Fin} } X \land A \ne \O}$
Thus by definition:
:$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is a non-empty set.
Let $x, y \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
Then
:$\exists A \in \map {\operatorname {Fin} } X: x = \sup A$ and $A \ne \O$
and
:$\exists B \in \map {\operatorname {Fin} } X: y = \sup B$ and $B \ne \O$
By Finite Union of Finite Sets is Finite:
:$A \cup B$ is finite
By Union of Subsets is Subset:
:$A \cup B \subseteq X$
By definitions of non-empty set and union:
:$A \cup B \ne \O$
By definition of $\operatorname {Fin}$:
:$\map \sup {A \cup B} \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
By Set is Subset of Union:
:$A \subseteq A \cup B$ and $B \subseteq A \cup B$
Thus by Supremum of Subset:
:$x \preceq \map \sup {A \cup B}$ and $y \preceq \map \sup {A \cup B}$
Thus by definition:
:$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
{{qed}}
Theorem: Change of Index Variable of Summation

:$\ds \sum_{\map R i} a_i = \sum_{\map R j} a_j$

Proof:
{{ProofWanted|Too obvious?}}
Theorem: Singleton is Finite

Let $x$ be arbitrary.
Then $\set x$ is a finite set.

Proof:
Define a mapping $f: \set x \to \N_{< 1}$:
:$\map f x = 0$
By definition of singleton:
:$\forall y, z \in \set x: \map f y = \map f z \implies y = z$
By definition:
:$f$ is an injection.
By definition of initial segment of natural numbers:
:$\N_{< 1} = \set 0$
By definition of $f$:
:$\forall n \in N_{< 1}: \exists z \in \set x: \map f z = n$
By definition:
:$f$ is a surjection.
By definition:
:$f$ is a bijection.
By definition of set equivalence:
:$\set x \sim \N_{< 1}$
Thus by definition:
:$\set x$ is a finite set.
{{qed}}
Theorem: Normal Property is Weakly Hereditary

If $T$ is a normal space then $T_K$ is also a normal space.
That is, the property of being a normal space is weakly hereditary.

Proof:
{{Recall|Normal Space|normal space|index = 1}}
{{:Definition:Normal Space/Definition 1}}
From $T_1$ Property is Hereditary, an arbitrary subspace of a $T_1$ space is also a $T_1$ space.
From $T_4$ Property is Weakly Hereditary, an arbitrary closed subspace of a $T_4$ space is also a $T_4$ space.
Hence the result.
{{qed}}
Theorem: Derivative of Natural Logarithm Function/Proof 4/Lemma

Let $\sequence {f_n}_n$ be the sequence of real functions $f_n: \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1}$
Let $k \in \N$.
Let $J = \closedint {\dfrac 1 k} k$.
Then the sequence of derivatives $\sequence { {f_n}'}_n$ converges uniformly to some real function $g: J \to \R$.

Proof:
From Derivative of $n$th Root and Combination Theorem for Sequences:
:$\forall n \in \N: \forall x \in J : D_x \map {f_n} x = \dfrac {\sqrt [n] x} x$
From Closed Bounded Subset of Real Numbers is Compact, $J$ is compact.
Thus:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} D_x \map {f_n} x
      | r = \lim_{n \mathop \to \infty} \dfrac {\sqrt [n] x} x
      | c = from above
}}
{{eqn | r = \frac 1 x \lim_{n \mathop \to \infty} \sqrt [n] x
      | c = Multiple Rule for Real Sequences
}}
{{eqn | r = \frac 1 x \lim_{n \mathop \to \infty} x^{1/n}
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | r = \frac 1 x
      | c = Power Function tends to One as Power tends to Zero: Rational Number
}}
{{end-eqn}}
In particular, $\sequence { {f_n}'}_n$ is pointwise convergent to a continuous function on $J$.
For $x \in \closedint {\frac 1 k} 1$:
{{begin-eqn}}
{{eqn | l = x^{1/n}
      | o = \le
      | r = x^{1 / \paren {n + 1} }
      | c = Exponential is Monotonic: Rational Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [n] x
      | o = \le
      | r = \sqrt [n + 1] x
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\sqrt [n] x} x
      | o = \le
      | r = \frac {\sqrt [n + 1] x} x
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{end-eqn}}
So $\sequence {\map { {f_n}'} x}_n$ is increasing when $x \in \closedint {\dfrac 1 k} 1$.
For $x \in \closedint 1 k$:
{{begin-eqn}}
{{eqn | l = x^{1/n}
      | o = \ge
      | r = x^{1 / \paren {n + 1} }
      | c = Exponential is Monotonic: Rational Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [n] x
      | o = \ge
      | r = \sqrt [n + 1] x
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\sqrt [n] x} x
      | o = \ge
      | r = \frac {\sqrt [n + 1] x} x
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{end-eqn}}
So $\sequence {\map { {f_n}'} x}_n$ is decreasing when $x \in \closedint {\dfrac 1 k} 1$.
Thus $\sequence {\map { {f_n}'} x}_n$ is monotone for all $x \in \closedint {\frac 1 k} 1 \cup \closedint 1 k = J$.
From Dini's Theorem, $\sequence { {f_n}'}_n$ converges uniformly to $\dfrac 1 x$ on $J$.
Hence the result.
{{qed}}
Category:Derivative of Natural Logarithm Function
l3nr447wjqopnurm2jfrv954hmkfo00
Theorem: Exponential Function is Well-Defined/Real

Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then $\exp x$ is well-defined.

Proof:
This proof assumes the power series definition of $\exp$.
From Series of Power over Factorial Converges:
:$\ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$ converges 
Hence the result, from Convergent Real Sequence has Unique Limit.
{{qed}}
Theorem: Exponential Function is Well-Defined/Real

Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then $\exp x$ is well-defined.

Proof:
This proof assumes the sequence definition of $\exp$.
Let $\sequence {f_n}$ be the sequence of mappings $f_n : \R \to \R$ defined as:
:$\map {f_n} x = \paren {1 + \dfrac x n}^n$
Fix $x \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f_n} x
      | r = \paren {1 + \dfrac x n}^n
      | c = Definition of $\map {f_n} x$
}}
{{eqn | r = \sum_{k \mathop = 0}^n \binom n k \frac {x^k} {n^k} 
      | c = Binomial Theorem for Integral Index
}}
{{eqn | r = \sum_{k \mathop = 0}^n \frac {x^k} {k!} \frac {\paren n \times \paren {n - 1} \times \paren {n - 2} \times \cdots \paren {n - k + 1} }{n \times n \times n \times \cdots n}
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \sum_{k \mathop = 0}^n \frac {x^k} {k!} \paren 1 \paren {1 - \frac 1 n} \paren {1 - \frac 2 n} \cdots \paren {1 - \frac {k - 1} n}
}}
{{eqn | o = \le
      | r = \size {\sum_{k \mathop = 0}^n \frac {x^k} {k!} \paren 1 \paren {1 - \frac 1 n} \paren {1 - \frac 2 n} \cdots \paren {1 - \frac {k - 1} n} }
      | c = Negative of Absolute Value
}}
{{eqn | r = \sum_{k \mathop = 0}^n \frac {\size x^k} {k!} \paren 1 \paren {1 - \frac 1 n} \paren {1 - \frac 2 n} \cdots \paren {1 - \frac {k - 1} n}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 0}^n \frac {\size x^k} {k!}
      | c = Multiplication of Positive Number by Real Number Greater than One
}}
{{eqn | o = <
      | r = \sum_{k \mathop = 0}^\infty \frac {\size x^k} {k!}
      | c = Sum of positive terms is increasing
}}
{{eqn | o = <
      | r = \infty
      | c = Series of Power over Factorial Converges
}}
{{end-eqn}}
{{MissingLinks|Result about increasing series seems not to be up yet}}
Thus, $\sequence {\map {f_n} x}$ is bounded above.
From Exponential Sequence is Eventually Increasing:
:$\exists N \in \N: \sequence {\map {f_{N + n} } x}$ is increasing
From Monotone Convergence Theorem (Real Analysis), $\sequence {\map {f_{N + n} } x}$ converges to some $z \in \R$.
From Tail of Convergent Sequence, $\sequence {\map {f_n} x}$ converges to $z$.
Hence the result, from Limit of Real Function is Unique.
{{qed}}
Theorem: Exponential Function is Well-Defined/Real

Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then $\exp x$ is well-defined.

Proof:
This proof assumes the continuous extension definition of $\exp$.
Let $e$ denote Euler's number.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$f \left({r}\right) = e^r$
From Euler's Number to Rational Power permits Unique Continuous Extension, there exists a unique continuous extension of $f$ to $\R$.
Hence the result.
{{qed}}
Theorem: Exponential Function is Well-Defined/Real

Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then $\exp x$ is well-defined.

Proof:
This proof assumes the definition of the exponential as the inverse of the logarithm.
From Logarithm is Strictly Increasing, $\ln$ is strictly monotone on $\R_{>0}$.
From Inverse of Strictly Monotone Function, $f$ permits an inverse mapping.
Hence the result, from Inverse Mapping is Unique.
{{qed}}
Theorem: Exponential Function is Well-Defined/Real

Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then $\exp x$ is well-defined.

Proof:
This proof assumes the definition of $\exp$ as the solution to an initial value problem.
That is, suppose $\exp$ solves:
:$(1): \quad \dfrac \d {\d x} y = \map f {x, y}$
:$(2): \quad \map \exp 0 = 1$
on $\R$, where $\map f {x, y} = y$.
From Derivative of Exponential Function: Proof 4, the function $\phi : \R \to \R$ defined as:
:$\ds \map \phi x = \sum_{k \mathop = 0}^\infty \frac {x^k} {k!}$
satisfies $\map {\phi'} x = \map \phi x$.
So $\phi$ satisfies $(1)$.
From Exponential of Zero: Proof 3:
:$\map \phi 0 = 1$
So $\phi$ satisfies $(2)$.
Thus, $\phi$ is a solution to the initial value problem given.
From Exponential Function is Continuous: Proof 5 and $(1)$:
:$\phi$ is continuously differentiable on $\R$.
Because $\map f {x, \phi} = \phi$:
:$f$ is continuously differentiable on $\R^2$.
Thus, from Uniqueness of Continuously Differentiable Solution to Initial Value Problem, this solution is unique.
{{qed}}
Theorem: Tail of Convergent Sequence

Let $\left\langle{a_n}\right\rangle$ be a real sequence.
Let $m \in \N$ be a natural number.
Let $a \in \R$ be a real number.
Then:
:$a_n \to a$
{{iff}}:
:$a_{n + m} \to a$

Proof:
=== Necessary Condition ===
Suppose that $a_n \to a$. 
Then for each $\epsilon > 0$, there exists $N \in \N$ such that: 
:$\size {a_n - a} < \epsilon$ for $n \ge N$. 
Set: 
:$N^\ast = \max \set {1, N - m}$ 
Then for $n \ge N^\ast$, we have $n \ge N - m$ and so $n + m \ge N$.
Then: 
:$\size {a_{n + m} - a} < \epsilon$ for $n \ge N^\ast$. 
So $a_{n + m} \to a$.
{{qed|lemma}}
Theorem: Union of Inverses of Mappings is Inverse of Union of Mappings

Let $I$ be an indexing set.
Let $\family {f_i: i \in I}$ be an indexed family of mappings.
For each $i \in I$, let $f^{-1}$ denote the inverse of $f$.
Then the inverse of the union of $\family {f_i: i \in I}$ is the union of the inverses of $f_i, i \in I$.
That is:
:$\ds \paren {\bigcup \family {f_i: i \in I} }^{-1} = \bigcup \family {f_i^{-1}: i \in I}$

Proof:
{{begin-eqn}}
{{eqn | l = \tuple {y, x}
      | o = \in
      | r = \paren {\bigcup \family {f_i: i \in I} }^{-1}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = \family {f_i: i \in I}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = \tuple {x, y}
      | o = \in
      | r = f_i
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = \tuple {y, x}
      | o = \in
      | r = f_i^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {y, x}
      | o = \in
      | r = \bigcup \family {f_i^{-1}: i \in I}
      | c = {{Defof|Union of Family}}
}}
{{end-eqn}}
{{qed}}
Category:Inverse Relations
Category:Set Union
Category:Indexed Families
sjg9fnvk4rbwja1puz5x352rnywj942
Theorem: Union of Functions Theorem/Corollary

For each $i \in \N$, let $g_i : X_i \to Y$ be invertible.
Then $\ds \bigcup \set {g_i: i \in \N}$ is invertible and:
:$\ds \paren {\bigcup \set {g_i: i \in \N} }^{-1} = \bigcup \set {g_i^{-1}: i \in \N}$

Proof:
{{ProofWanted}}
Category:Inverse Mappings
943qyuq5ivgtxh7mueilwt404u2vfoh
Theorem: Permutation of Indices of Summation

:$\ds \sum_{\map R j} a_j = \sum_{\map R {\map \pi j} } a_{\map \pi j}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{\map R {\map \pi j} } a_{\map \pi j}
      | r = \sum_{j \mathop \in \Z} a_{\map \pi j} \sqbrk {\map R {\map \pi j} }
      | c = {{Defof|Summation by Iverson's Convention}}
}}
{{eqn | r = \sum_{j \mathop \in \Z} \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i} \sqbrk {i = \map \pi j}
      | c = 
}}
{{eqn | r = \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i} \sum_{j \mathop \in \Z} \sqbrk {i = \map \pi j}
      | c = 
}}
{{eqn | r = \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i}
      | c = 
}}
{{eqn | r = \sum_{\map R i} a_i
      | c = 
}}
{{eqn | r = \sum_{\map R j} a_j
      | c = Change of Index Variable of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Translation of Index Variable of Summation

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \sum_{\map R j} a_j$ denote a summation over $R$.
Then:
:$\ds \sum_{\map R j} a_j = \sum_{\map R {c \mathop + j} } a_{c \mathop + j} = \sum_{\map R {c \mathop - j} } a_{c \mathop - j}$
where $c$ is an integer constant which is not dependent upon $j$.

Proof:
First we consider the case where the fiber of truth of $R$ is finite.
{{ProofWanted}}
Theorem: Axiom of Approximation in Up-Complete Semilattice

Let $\mathscr S = \struct {S, \wedge, \preceq}$ be an up-complete meet semilattice.
Let:
:$\forall x \in S: x^\ll$ is directed
Then:
:$\mathscr S$ satisfies the axiom of approximation
{{iff}}:
:$\forall x, y \in S: x \npreceq y \implies \exists u \in S: u \ll x \land u \npreceq y$

Proof:
=== Sufficient Condition ===
Let $\mathscr S$ satisfy the axiom of approximation.
Let $x, y \in S$ such that
:$x \npreceq y$
By assumption:
:$x^\ll$ is directed.
By definition of up-complete:
:$x^\ll$ admits a supremum.
By the axiom of approximation:
:$x = \map \sup {x^\ll}$
By definition of supremum:
:if $y$ is upper bound for $x^\ll$, then $x \preceq y$
By definition of upper bound:
:$\exists u \in x^\ll: u \npreceq y$
Thus by definition of way below closure:
:$\exists u \in S: u \ll x \land u \npreceq y$
{{qed|lemma}}
Theorem: Operand is Upper Bound of Way Below Closure

Let $\struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then
:$x$ is upper bound for $x^\ll$
where $x^\ll$ denotes the way below closure of $x$.

Proof:
Let $y \in x^\ll$
By definition of way below closure:
:$y \ll x$
where $\ll$ denotes the way below relation.
Thus by Way Below implies Preceding:
:$y \preceq x$
Thus by definition:
:$x$ is upper bound for $x^\ll$
{{qed}}