avewright/proofwiki-math huggingface dataset:
Theorem: Two Lines Meet at Unique Point

Let two straight line segments be constructed on a straight line segment from its endpoints so that they meet at a point.
Then there cannot be two other straight line segments equal to the former two respectively, constructed on the same straight line segment and on the same side of it, meeting at a different point.
{{:Euclid:Proposition/I/7}}

Proof:
:400px
Let $AC$ and $CB$ be constructed on $AB$ meeting at $C$.
Let two other straight line segments $AD$ and $DB$ be constructed on $AB$, on the same side of it, meeting at $D$, such that $AC = AD$ and $CB = DB$.
{{AimForCont}} $C$ and $D$ are different points.
Let $CD$ be joined.
We have {{hypothesis}} that:
:$AC = AD$
Hence from {{EuclidPropLink|prop = 5|title = Isosceles Triangle has Two Equal Angles}}:
:$\angle ACD = \angle ADC$
From {{EuclidCommonNotionLink|5}}:
:$\angle ACD > \angle DCB$ because the whole is greater than the part.
Therefore:
:$\angle CDB > \angle DCB$
We have {{hypothesis}}:
:$CB = DB$
Hence it follows that:
:$\angle CDB = \angle DCB$
But this contradicts:
:$\angle CDB > \angle DCB$
From this contradiction it follows that $C$ and $D$ cannot be different points.
Hence the result.
{{qed}}
{{Euclid Note|7|I}}
Theorem: Triangle Side-Side-Side Congruence

Let two triangles have all $3$ sides equal.
Then they also have all $3$ angles equal.
Thus two triangles whose sides are all equal are themselves congruent.
{{:Euclid:Proposition/I/8}}

Proof:
:500px
Let $\triangle ABC$ and $\triangle DEF$ be two triangles such that:
:$AB = DE$
:$AC = DF$
:$BC = EF$
Suppose $\triangle ABC$ were superimposed over $\triangle DEF$ so that point $B$ is placed on point $E$ and the side $BC$ on $EF$.
Then $C$ will coincide with $F$, as $BC = EF$ and so $BC$ coincides with $EF$.
{{AimForCont}} $BA$ does not coincide with $ED$ and $AC$ does not coincide with $DF$.
Then they will fall as, for example, $EG$ and $GF$.
Thus there will be two pairs of straight line segments constructed on the same line segment, on the same side as it, meeting at different points.
But from {{EuclidPropLink|prop = 7|title = Two Lines Meet at Unique Point}}, these points are coincident.
It follows by Proof by Contradiction that:
:$BA$ coincides with $ED$
:$AC$ coincides with $DF$.
Therefore $\angle BAC$ coincides with $\angle EDF$ and therefore:
:$\angle BAC = \angle EDF$
The same argument can be applied {{mutatis}} to the other two sides.
Thus we have shown that all corresponding angles are equal.
{{qed}}
Theorem: Triangle Side-Side-Side Congruence

Let two triangles have all $3$ sides equal.
Then they also have all $3$ angles equal.
Thus two triangles whose sides are all equal are themselves congruent.
{{:Euclid:Proposition/I/8}}

Proof:
Let $\triangle ABC$ and $\triangle DEF$ have all three pairs of corresponding sides equal.
Let $AC$ be the longest side of $\triangle ABC$.  
If there is more than one longest side, choose an arbitrary one.
We have {{hypothesis}}:
:$AC = DF$
{{tidy}}
There are two cases:
'''case 1'''
The two triangles can be arranged as shown.  They are reflections.
:200px
'''case 2'''
Otherwise, they are superimposable by the method in Triangle Side-Angle-Side Congruence).
In the words of Euclid (Euclid:Proposition/I/4:
:"If the triangle ABC is superposed on the triangle DEF, and if the point A is placed on the point D and the straight line AB on DE, then the point B also coincides with E, because AB equals DE..."
If so, then reflect $\triangle DEF$ in $DF$.
Now arrange $\triangle ABC$ and $\triangle DEF$ with $AC = DF$ shared, as shown in the figure.
Construct $BE$.
We have {{hypothesis}}:
:$AB = AE$
:$BC = EC$
By the definition of isosceles triangles:
:$\triangle ABE$ and $\triangle BEC$ are both isosceles.
By Isosceles Triangle has Two Equal Angles:
:$\angle ABE = \angle AEB$
:$\angle EBC = \angle BEC$
By addition:
:$\angle ABC = \angle AEC$
By Triangle Side-Angle-Side Congruence:
:$\triangle ABC \cong \triangle DEF$
{{qed}}
Theorem: Bisection of Angle

It is possible to bisect any given rectilineal angle.
{{:Euclid:Proposition/I/9}}

Proof:
We have:
:$AD = AE$
:$AF$ is common
:$DF = EF$
Thus from {{EuclidPropLink|prop = 8|title = Triangle Side-Side-Side Congruence}}:
:$\triangle ADF \sim \triangle AEF$
Thus:
:$\angle DAF = \angle EAF$
Hence $\angle BAC$ has been bisected by $AF$.
{{qed}}
{{Euclid Note|9|I|There are quicker and easier constructions of a bisection, but this particular one uses only results previously demonstrated.}}
Theorem: Bisection of Straight Line

It is possible to bisect a straight line segment.
{{:Euclid:Proposition/I/10}}

Proof:
As $\triangle ABC$ is an equilateral triangle, it follows that $AC = CB$.
The two triangles $\triangle ACD$ and $\triangle BCD$ have side $CD$ in common, and side $AC$ of $\triangle ACD$ equals side $BC$ of $\triangle BCD$.
The angle $\angle ACD$ subtended by lines $AC$ and $CD$ equals the angle $\angle BCD$ subtended by lines $BC$ and $CD$, as $\angle ACB$ was bisected.
So triangles $\triangle ACD$ and $\triangle BCD$ are equal.
Therefore $AD = DB$.
So $AB$ has been bisected at the point $D$.
{{qed}}
{{Euclid Note|10|I}}
Theorem: External Angle of Triangle is Greater than Internal Opposite

The external angle of a triangle is greater than either of the opposite internal angles.
{{:Euclid:Proposition/I/16}}

Proof:
:250px
Let $\triangle ABC$ be a triangle.
Let the side $BC$ be extended to $D$.
Let $AC$ be bisected at $E$.
Let $BE$ be joined and extended to $F$.
Let $EF$ be made equal to $BE$.
(Technically we really need to extend $BE$ to a point beyond $F$ and then crimp off a length $EF$.)
Let $CF$ be joined.
Let $AC$ be extended to $G$.
We have $\angle AEB = \angle CEF$ from Two Straight Lines make Equal Opposite Angles.
Since $AE = EC$ and $BE = EF$, from Triangle Side-Angle-Side Congruence we have $\triangle ABE = \triangle CFE$.
Thus $AB = CF$ and $\angle BAE = \angle ECF$.
But $\angle ECD$ is greater than $\angle ECF$.
Therefore $\angle ACD$ is greater than $\angle BAE$.
Similarly, if $BC$ were bisected, $\angle BCG$, which is equal to $\angle ACD$ by Two Straight Lines make Equal Opposite Angles, would be shown to be greater than $\angle ABC$ as well.
Hence the result.
{{qed}}
{{Euclid Note|16|I}}
Theorem: Limit iff Limits from Left and Right

Let $f$ be a real function defined on an open interval $\openint a b$ except possibly at a point $c \in \openint a b$.
Then:
:$\map f x \to l$ as $x \to c$
{{iff}}:
:$\map f x \to l$ as $x \to c^-$
and
:$\map f x \to l$ as $x \to c^+$

Proof:
=== Necessary Condition ===
Let $\map f x \to l$ as $x \to c$.
Then from the definition of the limit of a function:
:$\forall \epsilon > 0: \exists \delta > 0: 0 < \size {x - c} < \delta \implies \size {\map f x - l} < \epsilon$
So for any given $\epsilon$, there exists a $\delta$ such that:
:$0 < \size {x - c} < \delta$
implies that:
:$l - \epsilon < \map f x < l + \epsilon$
Now:
{{begin-eqn}}
{{eqn | o = 
      | r = 0 < \size {x - c} < \delta
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | r = - \delta < -\paren {x - c} < 0
      | c = 
}}
{{eqn | l = \lor
      | o = 
      | r = 0 < \paren {x - c} < \delta
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | r = c - \delta < x < c
      | c = 
}}
{{eqn | l = \lor
      | o = 
      | r = c < x < c + \delta
      | c = 
}}
{{end-eqn}}
That is: $\forall \epsilon > 0: \exists \delta > 0$:
:$(1): \quad c - \delta < x < c \implies \norm {\map f x - l} < \epsilon$
:$(2): \quad c < x < c + \delta \implies \norm {\map f x - l} < \epsilon$
So given that particular value of $\epsilon$, we can find a value of $\delta$ such that the conditions for both:
:$(1): \quad f$ tending to the limit $l$ as $x$ tends to $c$ from the left
and :
:$(2): \quad f$ tending to the limit $l$ as $x$ tends to $c$ from the right.
Thus:
:$\ds \lim_{x \mathop \to c} \map f x = l$
implies that:
:$\ds \lim_{x \mathop \to c^-} \map f x = l$
and:
:$\ds \lim_{x \mathop \to c^+} \map f x = l$
{{qed|lemma}}
Theorem: Limit of Function by Convergent Sequences

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $S \subseteq A_1$ be an open set of $M_1$.
Let $f: S \to A_2$ be a mapping defined on $S$, except possibly at the point $c \in S$.
Then $\ds \lim_{x \mathop \to c} \map f x = l$ {{iff}}:
:for each sequence $\sequence {x_n}$ of points of $S$ such that $\forall n \in \N_{>0}: x_n \ne c$ and $\ds \lim_{n \mathop \to \infty} x_n = c$
it is true that:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$

Proof:
=== Necessary Condition ===
Suppose that:
:$\ds \lim_{x \mathop \to c} \map f x = l$
Let $\epsilon > 0$.
Then by the definition of the limit of a mapping:
:$\exists \delta > 0: \map {d_2} {\map f x, l} < \epsilon$
provided $0 < \map {d_1} {x, c} < \delta$.
Now suppose that $\sequence {x_n}$ is a sequence of points of $S$ such that such that:
:$\forall n \in \N_{>0}: x_n \ne c$ and $\ds \lim_{n \mathop \to \infty} x_n = c$
Since $\delta > 0$, from the definition of the limit of a sequence:
:$\exists N \in \N_{>0}: \forall n > N: \map {d_1} {x_n, c} < \delta$
But:
:$\forall n \in \N_{>0}: x_n \ne c$
That means:
:$0 < \map {d_1} {x_n, c} < \delta$
by the definition of a metric.
But that implies:
:$\map {d_2} {\map f {x_n}, l} < \epsilon$
That is, given a value of $\epsilon > 0$, we have found a value of $N$ such that:
:$\forall n > N: \map {d_2} {\map f {x_n}, l} < \epsilon$
Thus:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
{{qed|lemma}}
Theorem: Real Polynomial Function is Continuous

A (real) polynomial function is continuous at every point.
Thus a (real) polynomial function is continuous on every interval of $\R$.

Proof:
Let $f_n$ be an arbitrary real polynomial function of degree $n$.
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$f_n$ is continuous on $\R$.
$\map P 0$ is the case $f_0$, where $f_0$ is of zero degree.
Such a real polynomial function is a constant function.
It follows from Constant Real Function is Continuous that $f_0$ is continuous on $\R$.
Thus $\map P 0$ is seen to hold.
=== Basis for the Induction ===
$\map P 1$ is the case:
:$f_1$ is continuous on $\R$.
Such a real polynomial function is a linear function.
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:An arbitrary real polynomial function of degree $k$ is continuous on $\R$
from which it is to be shown that:
:An arbitrary real polynomial function of degree $k + 1$ is continuous on $\R$.
=== Induction Step ===
This is the induction step:
:$\forall x \in \R: \map {f_{k + 1} } x = a_{k + 1} x^{k + 1} + \map {f_k} x$
for some real polynomial function of degree $k$, where $a_{k + 1} \in \R$
From the induction hypothesis $f_k$ is continuous on $\R$.
From Real Power Function for Positive Integer Power is Continuous, the real function $x \mapsto x^{k + 1}$ is continuous.
Hence from the Combined Sum Rule for Continuous Real Functions:
:$f_{k + 1}$ is continuous.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: f_n$ is continuous on $\R$.
{{qed}}
Theorem: Linear Function is Continuous

Let $\alpha, \beta \in \R$ be real numbers.
Let $f : \R \to \R$ be a linear real function:
:$\map f x = \alpha x + \beta$
for all $x \in \R$.
Then $f$ is continuous at every real number $c \in \R$.

Proof:
First assume $\alpha \ne 0$.
Let $\epsilon \in \R_{>0}$.
Let $\delta = \dfrac \epsilon {\size \alpha}$.
Then, provided that $\size {x - c} < \delta$:
{{begin-eqn}}
{{eqn | l = \size {\map f x - \map f c}
      | r = \size {\alpha \paren {x - c} }
      | c = 
}}
{{eqn | r = \size {\alpha} \cdot \size {x - c}
      | c = 
}}
{{eqn | o = <
      | r = \size {\alpha} \delta
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
So, we have found a $\delta$ for a given $\epsilon$ so as to make $\size {\map f x - \map f c} < \epsilon$ provided $\size {x - c} < \delta$.
So $\ds \lim_{x \mathop \to c} \map f x = \map f c$ and so $f$ is continuous at $c$, whatever $c$ happens to be.
Now suppose $\alpha = 0$.
Then $\forall x \in \R: \map f x - \map f c = 0$.
So whatever $\epsilon \in \R_{>0}$ we care to choose, $\size {\map f x - \map f c} < \epsilon$, and whatever $\delta$ may happen to be is irrelevant.
Continuity follows for all $c \in \R$, as above.
{{qed}}
Theorem: Linear Function is Continuous

Let $\alpha, \beta \in \R$ be real numbers.
Let $f : \R \to \R$ be a linear real function:
:$\map f x = \alpha x + \beta$
for all $x \in \R$.
Then $f$ is continuous at every real number $c \in \R$.

Proof:
Let $c \in \R$. 
Let $\sequence {x_n}$ be a real sequence converging to $c$. 
Then:
{{begin-eqn}}
{{eqn	| l = \lim_{n \mathop \to \infty} \map f {x_n}
	| r = \lim_{n \mathop \to \infty} \paren {\alpha x_n + \beta}
}}
{{eqn	| r = \alpha c + \beta
	| c = Combined Sum Rule for Real Sequences
}}
{{eqn	| r = \map f c
}}
{{end-eqn}}
We therefore have: 
:for all real sequences $\sequence {x_n}$ converging to $c$, the sequence $\sequence {\map f {x_n} }$ converges to $\map f c$.
So by Sequential Continuity is Equivalent to Continuity in the Reals $f$ is continuous at $c$. 
As $c \in \R$ was arbitrary, $f$ is continuous on $\R$.
{{qed}}
Theorem: Real Rational Function is Continuous

A real rational function is continuous at every point at which it is defined.
Thus a real rational function is continuous on every interval of $\R$ not containing a root of the denominator of the function.

Proof:
Let:
:$\map R x = \dfrac {\map P x} {\map Q x}$
be a real rational function, defined at all points of $\R$ at which $\map Q x \ne 0$.
Let $c \in \R$.
From Real Polynomial Function is Continuous:
:$\ds \lim_{x \mathop \to c} \map P x = \map P c$
and:
:$\ds \lim_{x \mathop \to c} \map Q x = \map Q c$
Thus by Quotient Rule for Limits of Real Functions:
:$\ds \lim_{x \mathop \to c} \map R x = \lim_{x \mathop \to c} \frac {\map P x} {\map Q x} = \frac {\map P c} {\map Q c}$
whenever $\map Q c \ne 0$.
So whatever value we choose for $c$ such that $\map Q c \ne 0$, we have that $\map P x$ is continuous at $c$.
From the definition of continuity on an interval, the second assertion follows.
{{qed}}
Theorem: Limit of Composite Function

Let $f$ and $g$ be real functions.
Let:
{{begin-eqn}}
{{eqn | l = \ds \lim_{y \mathop \to \eta} \map f y
      | r = l
}}
{{eqn | l = \ds \lim_{x \mathop \to \xi} \map g x
      | r = \eta
}}
{{end-eqn}}
Then, if either:
:'''Hypothesis 1:''' $f$ is continuous at $\eta$ (that is $l = \map f \eta$)
or:
:'''Hypothesis 2:''' for some open interval $I$ containing $\xi$, it is true that $\map g x \ne \eta$ for any $x \in I$ except possibly $x = \xi$
then:
:$\ds \lim_{x \mathop \to \xi} \map f {\map g x} = \lim_{y \mathop \to \eta} \map f y$

Proof:
Let $\epsilon > 0$.
Since $\ds \lim_{y \mathop \to \eta} \map f y = l$, we can find $\Delta > 0$ such that:
:$\size {\map f y - l} < \epsilon$ provided $0 < \size {y - \eta} < \Delta$
Let $y = \map g x$.
Then, provided that $0 < \size {\map g x - \eta} < \Delta$, we have:
:$\size {\map f {\map g x} - l} < \epsilon$
But $\ds \lim_{x \mathop \to \xi} \map g x = \eta$ and $\Delta > 0$.
Hence:
:$\exists \delta > 0: \size {\map g x - \eta} < \Delta$ provided that $0 < \size {x - \xi} < \delta$
We now need to establish the reason for the conditions under which $0 < \size {x - \xi} < \delta \implies \size {\map f {\map g x} - l} < \epsilon$.
Theorem: Condition for Continuity on Interval

Let $f$ be a real function defined on an interval $\mathbb I$.
Then $f$ is continuous on $\mathbb I$ {{iff}}:
:$\forall x \in \mathbb I: \forall \epsilon > 0: \exists \delta > 0: y \in \mathbb I \land \size {x - y} < \delta \implies \size {\map f x - \map f y} < \epsilon$

Proof:
Let $x \in \mathbb I$ such that $x$ is not an end point.
Then the condition $y \in \mathbb I \land \size {x - y} < \delta$ is the same as $\size {x - y} < \delta$ provided $\delta$ is small enough.
The criterion given therefore becomes the same as the statement $\ds \lim_{y \mathop \to x} \map f y = \map f x$, that is, that $f$ is continuous at $x$.
Now suppose $x \in \mathbb I$ and $x$ is a left hand end point of $\mathbb I$.
Then the condition $y \in \mathbb I \land \size {x - y} < \delta$ reduces to $x \le y < x + \delta$ provided $\delta$ is small enough.
The criterion given therefore becomes the same as the statement $\ds \lim_{y \mathop \to x^+} \map f y = \map f x$, that is, that $f$ is continuous on the right at $x$.
Similarly, if $x \in \mathbb I$ and $x$ is a right hand end point of $\mathbb I$, then the criterion reduces to the statement that $f$ is continuous on the left at $x$.
Thus the assertions are equivalent to the statement that $f$ is continuous at all points in $\mathbb I$, that is, that $f$ is continuous on $\mathbb I$.
{{qed}}
Theorem: Limit of Image of Sequence

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping which is continuous at $a \in A_1$.
Let $\sequence {x_n}$ be a sequence of points in $A_1$ such that:
:$\ds \lim_{n \mathop \to \infty} x_n = a$
where $\ds \lim_{n \mathop \to \infty} x_n$ is the limit of $x_n$.
Then:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = \map f a$
That is:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = \map f {\lim_{n \mathop \to \infty} x_n}$
That is, for a continuous mapping, the limit and function symbols commute.

Proof:
From Limit of Function by Convergent Sequences, we have:
:$\ds \lim_{x \mathop \to a} \map f x = \map f a$
{{iff}}:
:for each sequence $\sequence {x_n}$ of points of $A_1$ such that:
::$\forall n \in \N_{>0}: x_n \ne a$
:and:
::$\ds \lim_{n \mathop \to \infty} x_n = a$
:it is true that:
::$\ds \lim_{n \mathop \to \infty} \map f {x_n} = \map f a$
The result follows directly from this and the definition of continuity.
{{qed}}
Theorem: Image of Real Interval under Continuous Real Function is Real Interval

Let $I$ be a real interval.
Let $f: I \to \R$ be a continuous real function.
Then the image of $f$ is a real interval.

Proof:
Let $J$ be the image of $f$.
By definition of real interval, it suffices to show that:
:$\forall y_1, y_2 \in J: \forall \lambda \in \R: y_1 \le \lambda \le y_2 \implies \lambda \in J$
So suppose $y_1, y_2 \in J$, and suppose $\lambda \in \R$ is such that $y_1 \le \lambda \le y_2$.
Consider these subsets of $I$:
:$S = \set {x \in I: \map f x \le \lambda}$
:$T = \set {x \in I: \map f x \ge \lambda}$
As $y_1 \in S$ and $y_2 \in T$, it follows that $S$ and $T$ are both non-empty.
Also, $I = S \cup T$.
So from Interval Divided into Subsets, a point in one subset is at zero distance from the other.
So, suppose that $s \in S$ is at zero distance from $T$.
From Limit of Sequence to Zero Distance Point, we can find a sequence $\sequence {t_n}$ in $T$ such that $\ds  \lim_{n \mathop \to \infty} t_n = s$.
Since $f$ is continuous on $I$, it follows from Limit of Image of Sequence that:
:$\ds  \lim_{n \mathop \to \infty} \map f {t_n} = \map f s$
But:
:$\forall n \in \N_{> 0}: \map f {t_n} \ge \lambda$
Therefore by Lower and Upper Bounds for Sequences:
:$\map f s \ge \lambda$
We already have that:
:$\map f s \le \lambda$
Therefore:
:$\map f s = \lambda$
and so:
:$\lambda \in J$
A similar argument applies if a point of $T$ is at zero distance from $S$.
{{qed}}
Theorem: Image of Real Interval under Continuous Real Function is Real Interval

Let $I$ be a real interval.
Let $f: I \to \R$ be a continuous real function.
Then the image of $f$ is a real interval.

Proof:
Let $J$ be the image of $f$.
By Subset of Real Numbers is Interval iff Connected we need to show that $J$ is connected (and hence an interval).
{{AimForCont}} not.
Then there exists a separation $S \mid T$ of $J$.
Define $A = f^{-1} \sqbrk S$ and $B = f^{-1} \sqbrk T$. $A$ and $B$ are both non-empty.
Because $f$ is continuous, by Continuous iff inverse image of any open set is open we must have $A$ and $B$ open.
Because $S \mid T$ is a separation:
:$A \cap B = f^{-1} \sqbrk S \cap f^{-1} \sqbrk T = f^{-1} \sqbrk {S \cap T} = \O$, because $S \mid T$ is a separation.
Also, $A \cup B = f^{-1} \sqbrk S \cup f^{-1} \sqbrk T = f^{-1} \sqbrk {S \cup T} = f^{-1}(J) = I$ ($S \mid T$ is a separation of $J$).
Hence $A \mid B$ is a separation of $I$.
$I$ can certainly not be an interval (because it is not connected).
This is a contradiction.
Thus $J$ must be an interval.
{{qed}}
Theorem: Interval Divided into Subsets

Let $\mathbb I$ be a real interval.
Let $S$ and $T$ be non-empty subsets of $\mathbb I$ such that $\mathbb I \subseteq S \cup T$.
Then one of $S$ or $T$ contains an element at zero distance from the other.

Proof:
$\mathbb I \subseteq S \cup T \implies \forall x \in \mathbb I: x \in S \lor x \in T$ from the definition of union.
That is, every element of $\mathbb I$ belongs either to $S$ or to $T$.
The distance of an element $c \in \R$ from a subset $S$ of $\R$ is given as:
:$\ds \map d {c, S} = \map {\inf_{x \mathop \in S} } {\size {c - x} }$
Assume that $S$ and $T$ have no element in common, otherwise the result is trivial.
{{WLOG}}, suppose that $\exists s \in S, t \in T$ such that $s < t$.
(If not, then $\exists s \in S, t \in T$ such that $s > t$, and the following argument may be amended appropriately.)
Let $T_0 = \set {x: x \in T: x > s}$.
As $t \in T_0$ it follows that $T_0 \ne \O$.
Also, $T_0$ is bounded below by $s$.
Let $b = \map \inf {T_0}$.
If $b \notin T$ then $b \in S$.
But from Distance from Subset of Real Numbers, it follows that $\map d {b, T_0} = 0$.
Thus we have found an element in $S$ which is zero distance from $T$.
Otherwise, $b \in T$.
Then $b > s$, and the open interval $\openint s b$ is a non-empty subset of $S$.
Hence $b$ is an element in $T$ which is zero distance from $S$.
{{Qed}}
Theorem: Distance from Subset of Real Numbers

Let $S$ be a subset of the set of real numbers $\R$.
Let $x \in \R$ be a real number.
Let $\map d {x, S}$ be the distance between $x$ and $S$.
Then:

Proof:
From the definition of distance:
:$\forall x, y \in \R: \map d {x, y} = \size {x - y}$
Thus:
:$\ds \map d {x, S} = \map {\inf_{y \mathop \in S} } {\size {x - y} }$
Consider the set $T = \set {\size {x - y}: y \in S}$.
This has $0$ as a lower bound as Absolute Value is Bounded Below by Zero.
So:
:$\ds \map d {x, S} = \map {\inf_{y \mathop \in S} } {\size {x - y} } \ge 0$
If $x \in S$ then:
:$\size {x - x} = 0 \in T$
and so:
:$\ds 0 \le \map {\inf_{y \mathop \in S} } {\map d {x, y} }$
Thus:
:$\ds \map d {x, S} = \map {\inf_{y \mathop \in S} } {\map d {x, y} } = 0$
{{Qed}}
Theorem: Distance from Subset of Real Numbers

Let $S$ be a subset of the set of real numbers $\R$.
Let $x \in \R$ be a real number.
Let $\map d {x, S}$ be the distance between $x$ and $S$.
Then:

Proof:
Recall from Real Number Line is Metric Space that the set of real numbers $\R$ with the distance function $d$ is a metric space.
The result is then seen to be an example of Distance from Subset to Element.
{{Qed}}
Theorem: Distance from Subset of Real Numbers

Let $S$ be a subset of the set of real numbers $\R$.
Let $x \in \R$ be a real number.
Let $\map d {x, S}$ be the distance between $x$ and $S$.
Then:

Proof:
From the definition of distance:
:$\forall x, y \in \R: \map d {x, y} = \size {x - y}$
Thus:
:$\ds \map d {x, S} = \map {\inf_{y \mathop \in S} } {\size {x - y} }$
Let $\xi = \inf S$.
Consider $\map d {-\xi, S'}$ where $S' = \set {-\xi: \xi \in S}$.
By Negative of Infimum is Supremum of Negatives:
:$\xi = \inf S \implies -\xi = \sup S'$
Thus from the above, $\map d {-\xi, S'} = 0$ and hence the result.
{{Qed}}
Theorem: Distance from Subset of Real Numbers

Let $S$ be a subset of the set of real numbers $\R$.
Let $x \in \R$ be a real number.
Let $\map d {x, S}$ be the distance between $x$ and $S$.
Then:

Proof:
Recall from Real Number Line is Metric Space that the set of real numbers $\R$ with the distance function $d$ is a metric space.
The result is then seen to be an example of Distance from Subset to Infimum.
{{Qed}}