avewright/proofwiki-math huggingface dataset:
Theorem: Isometry is Homeomorphism of Induced Topologies

Let $\struct {S_1, d_1}$ and $\struct {S_2, d_2}$ be metric spaces or pseudometric spaces.
Let $f: S_1 \to S_2$ be an isometry from $\struct {S_1, d_1}$ to $\struct {S_2, d_2}$.
Let $\tau_1$ and $\tau_2$ be the topologies induced on $S_1$ and $S_2$ by the metrics $d_1$ and $d_2$, respectively.
Then $f$ is a homeomorphism from $\struct {S_1, \tau_1}$ to $\struct {S_2, \tau_2}$.

Proof:
By the definition of an isometry, $f$ is bijective.
By Continuous Mapping is Continuous on Induced Topological Spaces, $f$ is a continuous mapping from $\struct {S_1, \tau_1}$ to $\struct {S_2, \tau_2}$.
{{explain|It needs to be established that $f$ is continuous on the original metric spaces in the first place.}}
By Inverse of Isometry of Metric Spaces is Isometry, $f^{-1}$ is an isometry.
By Continuous Mapping is Continuous on Induced Topological Spaces once more, $f^{-1}$ is a continuous mapping from $\struct {S_2, \tau_2}$ to $\struct {S_1, \tau_1}$.
Thus $f$ is a homeomorphism from $\struct {S_1, \tau_1}$ to $\struct {S_2, \tau_2}$.
{{qed}}
Category:Isometries (Metric Spaces)
Category:Homeomorphisms (Topological Spaces)
7q8n0g244zculgl6yo4gvxm0wfmoxco
Theorem: Equivalence of Definitions of Distributive Lattice

{{TFAE|def = Distributive Lattice}}
Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.

Proof:
In what follows it is shown that if one of the axioms distributive lattice axioms holds then they all hold.
Theorem: Distance-Preserving Surjection is Isometry of Metric Spaces

Let $M_1 = \left({A_1, d_1}\right)$ and $M_2 = \left({A_2, d_2}\right)$ be metric spaces.
Let $\phi: M_1 \to M_2$ be a surjective distance-preserving mapping.
That is:
:$\forall a, b \in M_1: d_1 \tuple {a, b} = d_2 \tuple {\map \phi a, \map \phi b}$
Then $\phi$ is an isometry.

Proof:
The premises satisfy all elements of the definition of isometry except for bijectivity.
As we presume $\phi$ to be surjective we need only show that it is injective.
By Distance-Preserving Mapping is Injection of Metric Spaces then $\phi$ is injective.
{{qed}}
Category:Isometries (Metric Spaces)
agrybp757xrenqh73ffdlcxafkvuabz
Theorem: Existence of Positive Root of Positive Real Number

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n \ne 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
=== Positive Exponent ===
{{:Existence of Positive Root of Positive Real Number/Positive Exponent|Positive Exponent}}
Theorem: Existence of Positive Root of Positive Real Number

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n \ne 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
Let $f$ be the real function defined on the unbounded closed interval $\hointr 0 \to$ defined by $\map f y = y^n$.
Consider first the case of $n > 0$.
By Strictly Positive Integer Power Function is Unbounded Above:
:$\exists q \in \R_{>0}: \map f q \ge x$
Since $x \ge 0$:
:$\map f 0 \le x$
By the Intermediate Value Theorem:
:$\exists y \in \R: 0 \le y \le q, \map f y = x$
Hence the result has been shown to hold for $n > 0$.
{{qed}}
Theorem: Existence of Positive Root of Positive Real Number

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n \ne 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
Let $S$ be the set consisting of the positive real numbers $t$ such that $t^n < x$.
Let $t = \dfrac x {1 - x}$.
Then $0 < t < 1$ and so:
:$t^n < t < x$
demonstrating that $S \ne \O$.
Let $t_0 = 1 + x$.
Then $t > t_0$ implies $t^n \ge t > x$.
So $t \notin S$.
Hence $t_0$ is an upper bound of $S$.
By the Continuum Property, $S$ has a supremum.
Let $y = \sup S$.
{{AimForCont}} $y_n < x$.
Choose $h \in \R$ such that $0 < h < 1$ and such that:
:$h < \dfrac {x - y^n} {\paren {1 + y}^n - y^n}$
Let $\dbinom n m$ denote a binomial coefficient.
By the Binomial Theorem, the coefficient of $z^m$ in the expansion of $\paren {1 + z}^n$ is
We have:
{{begin-eqn}}
{{eqn | l = \paren {y + h}^n
      | r = y^n + \dbinom n 1 y^{n - 1} h + \dbinom n 2 y^{n - 2} h^2 + \dotsb + \dbinom n n h^n
      | c = Binomial Theorem
}}
{{eqn | o = \le
      | r = y^n + h \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} + \dotsb + \dbinom n n}
      | c = as $0 < h < 1$
}}
{{eqn | r = y^n + h \paren {\paren {1 + y}^n - y^n}
      | c = Binomial Theorem
}}
{{eqn | o = <
      | r = y^n + \paren {x - y^n}
      | c = Definition of $h$
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Thus we have $y + h \in S$, which contradicts the fact that $y$ is an upper bound of $S$.
{{AimForCont}} $y^n > x$.
Let $k \in \R$ be chosen such that:
:$0 < k < 1$
:$k < y$
:$k < \dfrac {y^n - x} {\paren {1 + y}^n - y^n}$
Let $t \ge y - k$.
Then:
{{begin-eqn}}
{{eqn | l = t^n
      | o = \ge
      | r = \paren {y - k}^n
      | c = 
}}
{{eqn | r = y^n - \dbinom n 1 y^{n - 1} h + \dbinom n 2 y^{n - 2} h^2 - \dotsb + \paren {-1} \dbinom n n h^n
      | c = Binomial Theorem
}}
{{eqn | r = y^n - k \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} k - \dotsb + \paren {-1} \dbinom n n k^{n - 1} }
      | c = 
}}
{{eqn | o = \ge
      | r = y^n - k \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} + \dotsb + \dbinom n n}
      | c = as $0 < k < 1$
}}
{{eqn | r = y^n - k \paren {\paren {1 + y}^n - y^n}
      | c = Binomial Theorem
}}
{{eqn | o = >
      | r = y^n - \paren {y^n - x}
      | c = Definition of $k$
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Thus we have $y - k$ is an upper bound of $S$
This contradicts the fact that $y$ is the supremum of $S$.
It has been shown that both $y^n < x$ and $y^n > x$ lead to a contradiction.
Hence it must be the case that $y^n = x$.
Hence the result.
{{qed}}
Theorem: Proof by Cases/Formulation 2

:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r} }}
{{Assumption|1|\paren {p \implies r} \land \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \lor q} \implies r|1|Proof by Cases: Formulation 1: Forward Implication}}
{{Implication|3||\paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Proof by Cases/Formulation 2

:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccccc|c|ccccc|} \hline
((p & \implies & r) & \land & (q & \implies & r)) & \implies & ((p & \lor & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \T & \F & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Proof by Cases/Formulation 2

:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r} }}
{{TheoremIntro|1|\paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}|Proof by Cases: Forward Implication}}
{{TheoremIntro|2|\paren {\paren {p \lor q} \implies r} \implies \paren {\paren {p \implies r} \land \paren {q \implies r} }|Proof by Cases: Reverse Implication}}
{{BiconditionalIntro|3||\paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Proof by Cases/Formulation 2/Forward Implication

:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r} }}
{{Assumption|1|\paren {p \implies r} \land \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \lor q} \implies r|1|Proof by Cases: Formulation 1: Forward Implication}}
{{Implication|3||\paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Proof by Cases/Formulation 2/Forward Implication

:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccccc|c|ccccc|} \hline
((p & \implies & r) & \land & (q & \implies & r)) & \implies & ((p & \lor & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \T & \F & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Proof by Cases/Formulation 2/Reverse Implication

:$\vdash \paren {\paren {p \lor q} \implies r} \implies \paren {\paren {p \implies r} \land \paren {q \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \lor q} \implies r} \implies \paren {\paren {p \implies r} \land \paren {q \implies r} } }}
{{Assumption|1|\paren {p \lor q} \implies r}}
{{SequentIntro|2|1|\paren {p \implies r} \land \paren {q \implies r}|1|Proof by Cases: Formulation 1: Reverse Implication}}
{{Implication|3||\paren {\paren {p \lor q} \implies r} \implies \paren {\paren {p \implies r} \land \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Category:Proof by Cases
3x1etvtoecmzm510ircn7uf4d6ygy9r
Theorem: Set is Subset of Union/Set of Sets

Let $\mathbb S$ be a set of sets.
Then:
:$\ds \forall T \in \mathbb S: T \subseteq \bigcup \mathbb S$

Proof:
Let $T$ be any element of $\mathbb S$.
We wish to show that $T \subseteq S$.
Let $x \in T$.
Then: 
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = T
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup \mathbb S
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
Since this holds for each $x \in T$:
{{begin-eqn}}
{{eqn | l = T
      | o = \subseteq
      | r = \bigcup \mathbb S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
As $T$ was arbitrary, it follows that:
:$\forall T \in \mathbb S: T \subseteq \bigcup \mathbb S$
{{qed}}
Category:Set Union
Category:Subsets
2h884fzrg0phfpssv150hkszljbmxiw
Theorem: Proof by Cases/Formulation 3

:$\vdash \paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies r$

Proof:
{{BeginTableau|\paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies r}}
{{TheoremIntro|1|\paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s}|Constructive Dilemma: Formulation 3}}
{{Substitution|2||\paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies \paren {r \lor r}|1|r|q|q|r|s|r}}
{{Assumption|3|\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} }}
{{ModusPonens|4|3|r \lor r|2|3}}
{{Idempotence|5|3|r|4|Disjunction}}
{{Implication|6||\paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies r|3|5}}
{{EndTableau|qed}}
Theorem: Existence of Positive Root of Positive Real Number/Positive Exponent

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n > 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
Let $f$ be the real function defined on the unbounded closed interval $\hointr 0 \to$ defined by $\map f y = y^n$.
Consider first the case of $n > 0$.
By Strictly Positive Integer Power Function is Unbounded Above:
:$\exists q \in \R_{>0}: \map f q \ge x$
Since $x \ge 0$:
:$\map f 0 \le x$
By the Intermediate Value Theorem:
:$\exists y \in \R: 0 \le y \le q, \map f y = x$
Hence the result has been shown to hold for $n > 0$.
{{qed}}
Theorem: Existence of Positive Root of Positive Real Number/Positive Exponent

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n > 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
Let $S$ be the set consisting of the positive real numbers $t$ such that $t^n < x$.
Let $t = \dfrac x {1 - x}$.
Then $0 < t < 1$ and so:
:$t^n < t < x$
demonstrating that $S \ne \O$.
Let $t_0 = 1 + x$.
Then $t > t_0$ implies $t^n \ge t > x$.
So $t \notin S$.
Hence $t_0$ is an upper bound of $S$.
By the Continuum Property, $S$ has a supremum.
Let $y = \sup S$.
{{AimForCont}} $y_n < x$.
Choose $h \in \R$ such that $0 < h < 1$ and such that:
:$h < \dfrac {x - y^n} {\paren {1 + y}^n - y^n}$
Let $\dbinom n m$ denote a binomial coefficient.
By the Binomial Theorem, the coefficient of $z^m$ in the expansion of $\paren {1 + z}^n$ is
We have:
{{begin-eqn}}
{{eqn | l = \paren {y + h}^n
      | r = y^n + \dbinom n 1 y^{n - 1} h + \dbinom n 2 y^{n - 2} h^2 + \dotsb + \dbinom n n h^n
      | c = Binomial Theorem
}}
{{eqn | o = \le
      | r = y^n + h \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} + \dotsb + \dbinom n n}
      | c = as $0 < h < 1$
}}
{{eqn | r = y^n + h \paren {\paren {1 + y}^n - y^n}
      | c = Binomial Theorem
}}
{{eqn | o = <
      | r = y^n + \paren {x - y^n}
      | c = Definition of $h$
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Thus we have $y + h \in S$, which contradicts the fact that $y$ is an upper bound of $S$.
{{AimForCont}} $y^n > x$.
Let $k \in \R$ be chosen such that:
:$0 < k < 1$
:$k < y$
:$k < \dfrac {y^n - x} {\paren {1 + y}^n - y^n}$
Let $t \ge y - k$.
Then:
{{begin-eqn}}
{{eqn | l = t^n
      | o = \ge
      | r = \paren {y - k}^n
      | c = 
}}
{{eqn | r = y^n - \dbinom n 1 y^{n - 1} h + \dbinom n 2 y^{n - 2} h^2 - \dotsb + \paren {-1} \dbinom n n h^n
      | c = Binomial Theorem
}}
{{eqn | r = y^n - k \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} k - \dotsb + \paren {-1} \dbinom n n k^{n - 1} }
      | c = 
}}
{{eqn | o = \ge
      | r = y^n - k \paren {\dbinom n 1 y^{n - 1} + \dbinom n 2 y^{n - 2} + \dotsb + \dbinom n n}
      | c = as $0 < k < 1$
}}
{{eqn | r = y^n - k \paren {\paren {1 + y}^n - y^n}
      | c = Binomial Theorem
}}
{{eqn | o = >
      | r = y^n - \paren {y^n - x}
      | c = Definition of $k$
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Thus we have $y - k$ is an upper bound of $S$
This contradicts the fact that $y$ is the supremum of $S$.
It has been shown that both $y^n < x$ and $y^n > x$ lead to a contradiction.
Hence it must be the case that $y^n = x$.
Hence the result.
{{qed}}
Theorem: Existence of Positive Root of Positive Real Number/Negative Exponent

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n < 0$.
Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
Let $m = -n$.
Then $m > 0$.
Let $g$ be the real function defined on $\hointr 0 \to$ defined by:
:$\map g y = y^m$
Since $x \ge 0$:
:$\dfrac 1 x \ge 0$
By Existence of Positive Root of Positive Real Number: Positive Exponent there is a $y > 0$ such that:
:$\map g y = \dfrac 1 x$
It follows from the definition of power that:
{{begin-eqn}}
{{eqn | l = \map f y
      | r = \dfrac 1 {\map g y}
}}
{{eqn | r = \dfrac 1 {1 / x}
}}
{{eqn | r = x
}}
{{end-eqn}}
{{qed}}
Category:Existence of Positive Root of Positive Real Number
2ioe7yjmlsdu080btfmgrb6l8e72o6z
Theorem: Power of Ring Negative

Let $\struct {R, +, \circ}$ be a ring.
Let $n \in \N_{>0}$ be a strictly positive integer.
Let $x \in R$.
Then:
:If $n$ is even:
:::$\map {\circ^n} {-x} = \map {\circ^n} x$
:If $n$ is odd:
:::$\map {\circ^n} {-x} = -\map {\circ^n} x$

Proof:
First, suppose that $n$ is even.
Then for some $m \in \N_{>0}$:
:$n = 2 m = m + m$
Thus since $\circ$ is associative:
:$\ds \map {\circ^n} {-x} = \prod_{i \mathop = 1}^m \paren {-x} \circ \paren {-x}$
By Product of Ring Negatives:
:$\paren {-x} \circ \paren {-x} = x \circ x = \map {\circ^2} x$
Thus:
:$\ds \map {\circ^n} {-x} = \prod_{i \mathop = 1}^m \map {\circ^2} x$
By associativity:
:$\map {\circ^n} {-x} = \map {\circ^{2 m} } x = \map {\circ^n} x$
{{qed|lemma}}
Now suppose instead that $n$ is odd.
If $n = 1$, then:
:$\map {\circ^n} {-x} = -x = -\map {\circ^n} x$
Otherwise:
{{begin-eqn}}
{{eqn | l = \map {\circ^n} {-x}
      | r = \paren {-x} \circ \paren {\map {\circ^{n - 1} } {-x} }
}}
{{eqn | r = \paren {-x} \circ \paren {\map {\circ^{n - 1} } x}
      | c = $n-1$ is a strictly positive even integer, so the above case applies
}}
{{eqn | r = -\paren {x \circ \paren {\map {\circ^{n - 1} } x} }
      | c = Product with Ring Negative
}}
{{eqn | r = -\map {\circ^n} x
      | c = Definition of $\map {\circ^n} x$
}}
{{end-eqn}}
{{qed}}
Category:Ring Theory
Category:Powers
3f1qz79o1f5gzfymimd2i7483ubhtec
Theorem: Paving Lemma

Let $S$ be an open subset of the Euclidean space $\R^m$ or the set of complex numbers $\C$.
Let $\gamma: \closedint a b \to S$ be a path in $S$.
Then there exists $K \in \R_{>0}$ such that:
:For all $\epsilon \in \openint 0 K$, there exists a normal subdivision $\set {x_0, x_1, \ldots, x_{n - 1}, x_n}$ of the closed interval $\closedint a b$ such that:
::$\ds \bigcup_{i \mathop = 0}^n \map {B_\epsilon} {\map \gamma {x_i} } \subseteq S$
:and for all $i \in \set {0, 1, \ldots, n - 1}$:
::$\map \gamma {\closedint {x_i} {x_{i + 1} } } \subseteq \map {B_\epsilon} {\map \gamma {x_i} }$
Here, $\map {B_\epsilon} {\map \gamma {x_i} }$ denotes the open ball of $\map \gamma {x_i}$ with radius $\epsilon$.

Proof:
=== Finding the constant ===
First, suppose that $S$ is a subset of $\R^m$.
From Closed Real Interval is Compact in Metric Space, it follows that $\closedint a b$ is compact.
Then Continuous Image of Compact Space is Compact shows that $\map \gamma {\closedint {x_i} {x_{i + 1} } }$ is compact.
From the Heine-Borel Theorem, it follows that $\map \gamma {\closedint {x_i} {x_{i + 1} } }$ is bounded and closed.
Suppose that $S \ne \R^m$.
As $\R^m \setminus S$ is closed, it follows from Distance between Closed Sets in Euclidean Space that:
:$\map d {\map \gamma {\closedint a b}, \R^m \setminus S} > 0$
Put $K = \map d {\map \gamma {\closedint a b}, \R^m \setminus S}$, the distance between $\map \gamma {\closedint a b}$ and $\R^m \setminus S$.
If instead $S = \R^m$, then $K$ may be any strictly positive real number.
Theorem: Proof by Cases/Formulation 1/Reverse Implication

:$\paren {p \lor q} \implies r \vdash \paren {p \implies r} \land \paren {q \implies r}$

Proof:
{{BeginTableau|\paren {p \lor q} \implies r \vdash \paren {p \implies r} \land \paren {q \implies r} }}
{{Premise|1|\paren {p \lor q} \implies r}}
{{Assumption|2|p}}
{{Addition|3|2|p \lor q|2|1}}
{{ModusPonens|4|1, 2|r|1|3}}
{{Implication|5|1|p \implies r|2|4}}
{{Assumption|6|q}}
{{Addition|7|6|p \lor q|6|2}}
{{ModusPonens|8|1, 6|r|1|7}}
{{Implication|9|1|q \implies r|6|8}}
{{Conjunction|10|1|\paren {p \implies r} \land \paren {q \implies r}|5|9}}
{{EndTableau|qed}}
Category:Proof by Cases
3mmxy8qc87f2xgez8q3j2gihz3d6ilv
Theorem: Praeclarum Theorema/Formulation 1

:$\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s}$

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s} }}
{{Premise|1|\paren {p \implies q} \land \paren {r \implies s} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|r \implies s|1|2}}
{{Assumption|4|p \land r}}
{{Simplification|5|4|p|4|1}}
{{Simplification|6|4|r|4|2}}
{{ModusPonens|7|1, 4|q|2|5}}
{{ModusPonens|8|1, 4|s|3|6}}
{{Conjunction|9|1, 4|q \land s|7|8|}}
{{Implication|10|1|\paren {p \land r} \implies \paren {q \land s} |4|9}}
{{EndTableau|qed}}
Theorem: Praeclarum Theorema/Formulation 1

:$\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s}$

Proof:
{{BeginTableau   |\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s} }}
{{Premise        |1|\paren {p \implies q} \land \paren {r \implies s} }}
{{Simplification |2|1|p \implies q|1|1}}
{{Simplification |3|1|r \implies s|1|2}}
{{SequentIntro   |4|1|p \land r \implies q \land r|2|Factor Principles/Conjunction on Right/Formulation 1/Proof 2}}
{{SequentIntro   |5|1|q \land r \implies q \land s|3|Factor Principles/Conjunction on Left/Formulation 1/Proof 2}}
{{SequentIntro   |6|1|p \land r \implies q \land s|4, 5|Hypothetical Syllogism}}
{{EndTableau|qed}}
Theorem: Praeclarum Theorema/Formulation 1

:$\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen for all boolean interpretations by inspection, where the truth value under the main connective on the {{LHS}} is $T$, that under the one on the {{RHS}} is also $T$:
:<nowiki>$\begin{array}{|ccccccc||ccccccc|} \hline
(p & \implies & q) & \land & (r & \implies & s) & (p & \land & r) & \implies & (q & \land & s) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \F & \T & \T & \F & \F & \F & \T & \F & \F & \T \\
\F & \T & \F & \F & \T & \F & \F & \F & \F & \T & \T & \F & \F & \F \\
\F & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \F & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \F & \T & \T & \F & \F & \F & \T & \T & \T & \T \\
\F & \T & \T & \F & \T & \F & \F & \F & \F & \T & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \F & \F & \T & \T & \T & \F & \F & \T & \F & \F & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \F & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
Hence the result.
Note that the two formulas are not equivalent, as the relevant columns do not match exactly.
{{qed}}
Theorem: Praeclarum Theorema/Formulation 2

:$\vdash \paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} } }}
{{Assumption|1|\paren {\paren {p \implies q} \land \paren {r \implies s} } }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|r \implies s|1|2}}
{{Assumption|4|p \land r}}
{{Simplification|5|4|p|4|1}}
{{Simplification|6|4|r|4|2}}
{{ModusPonens|7|1, 4|q|2|5}}
{{ModusPonens|8|1, 4|s|3|6}}
{{Conjunction|9|1, 4|q \land s|7|8|}}
{{Implication|10|1|\paren {p \land r} \implies \paren {q \land s} |4|9}}
{{Implication|11||\paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} }|1|10}}
{{EndTableau|qed}}