avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Dilemma/Formulation 1/Forward Implication

:$\paren {p \implies q} \land \paren {\neg p \implies q} \vdash q$

Proof:
From the Constructive Dilemma we have:
:$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$
from which, changing the names of letters strategically:
:$p \implies q, \neg p \implies q \vdash p \lor \neg p \implies q \lor q$
From Law of Excluded Middle, we have:
:$\vdash p \lor \neg p$
From the Rule of Idempotence we have:
:$q \lor q \vdash q$
and the result follows by Hypothetical Syllogism.
{{qed}}
{{LEM||3}}
Theorem: Principle of Dilemma/Formulation 1/Reverse Implication

:$q \vdash \paren {p \implies q} \land \paren {\neg p \implies q}$

Proof:
{{BeginTableau|q \vdash \paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Premise|1|q}}
{{SequentIntro|2|1|p \implies q|1|True Statement is implied by Every Statement}}
{{SequentIntro|3|1|\neg p \implies q|1|True Statement is implied by Every Statement}}
{{Conjunction|4|1|\paren {p \implies q} \land \paren {\neg p \implies q}|2|3}}
{{EndTableau}}
{{qed}}
Category:Principle of Dilemma
38tgkfo4rswpxjpujfi94p1jjrp9a56
Theorem: Principle of Dilemma/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q}}
{{Assumption|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{SequentIntro|2|1|q|1|Principle of Dilemma: Formulation 1}}
{{Implication|3||\paren {p \implies q} \land \paren {\neg p \implies q} \implies q|1|2}}
{{EndTableau|qed}}
Theorem: Principle of Dilemma/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q}}
{{Assumption|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{Assumption|4|\neg q}}
{{ModusTollens|5|1, 4|\neg p|2|4}}
{{ModusPonens|6|1, 4|q|3|5}}
{{NonContradiction|7|1, 4|4|6}}
{{Contradiction|8|1|\neg \neg q|4|7}}
{{DoubleNegElimination|9|1|q|8}}
{{Implication|10||\paren {p \implies q} \land \paren {\neg p \implies q} \implies q|1|9}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Principle of Dilemma/Formulation 2/Forward Implication

:$\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q}}
{{Assumption|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{SequentIntro|2|1|q|1|Principle of Dilemma: Formulation 1}}
{{Implication|3||\paren {p \implies q} \land \paren {\neg p \implies q} \implies q|1|2}}
{{EndTableau|qed}}
Theorem: Principle of Dilemma/Formulation 2/Forward Implication

:$\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \land \paren {\neg p \implies q} \implies q}}
{{Assumption|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{Assumption|4|\neg q}}
{{ModusTollens|5|1, 4|\neg p|2|4}}
{{ModusPonens|6|1, 4|q|3|5}}
{{NonContradiction|7|1, 4|4|6}}
{{Contradiction|8|1|\neg \neg q|4|7}}
{{DoubleNegElimination|9|1|q|8}}
{{Implication|10||\paren {p \implies q} \land \paren {\neg p \implies q} \implies q|1|9}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Principle of Dilemma/Formulation 2/Reverse Implication

:$\vdash q \implies \paren {\paren {p \implies q} \land \paren {\neg p \implies q} }$

Proof:
{{BeginTableau|\vdash q \implies \paren {\paren {p \implies q} \land \paren {\neg p \implies q} } }}
{{Assumption|1|q|}}
{{SequentIntro|2|1|\paren {p \implies q} \land \paren {\neg p \implies q}|1|Principle of Dilemma: Formulation 1: Reverse Implication}}
{{Implication|3||q \implies \paren {\paren {p \implies q} \land \paren {\neg p \implies q} }|1|2}}
{{EndTableau}}
{{qed}}
Category:Principle of Dilemma
d9q4uvsexr57d799yi2aupfipflfpf2
Theorem: Open Domain is Connected iff it is Path-Connected

Let $D \subseteq \C$ be a open subset of the set of complex numbers.
Then $D$ is connected {{iff}} $D$ is path-connected.

Proof:
=== Necessary Condition ===
Complex Plane is Metric Space shows that $\C$ is topologically equivalent to the Euclidean space $\R^2$.
{{Corollary|Continuous Image of Connected Space is Connected|1}} shows that connectedness is a topological property.
The result follows from Connected Open Subset of Euclidean Space is Path-Connected.
{{qed|lemma}}
Theorem: Proof by Contradiction/Variant 2/Formulation 2

:$\vdash \paren {\paren {p \implies q} \land \paren {p \implies \neg q} } \implies \neg p$

Proof:
{{BeginTableau  |\vdash \paren {\paren {p \implies q} \land \paren {p \implies \neg q} } \implies \neg p}}
{{Assumption    |1|\paren {p \implies q} \land \paren {p \implies \neg q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|p \implies \neg q|1|2}}
{{Assumption    |4|p}}
{{ModusPonens   |5|1, 4|q|2|4}}
{{ModusPonens   |6|1, 4|\neg q|3|4}}
{{NonContradiction|7|1, 4 |5|6}}
{{Contradiction |8|1|\neg p|4|7}}
{{Implication   |9| |\paren {\paren {p \implies q} \land \paren {p \implies \neg q} } \implies \neg p|1|8}}
{{EndTableau|qed}}
Theorem: Proof by Contradiction/Variant 3/Formulation 2

:$\vdash \paren {p \implies \neg p} \implies \neg p$

Proof:
{{BeginTableau|\vdash \paren {p \implies \neg p} \implies \neg p}}
{{Assumption|1|p \implies \neg p}}
{{SequentIntro|2|1|\neg p|1|Proof by Contradiction: Variant 3: Formulation 1}}
{{Implication|3||\paren {p \implies \neg p} \implies \neg p|1|2}}
{{EndTableau|qed}}
Theorem: Proof by Contradiction/Variant 3/Formulation 2

:$\vdash \paren {p \implies \neg p} \implies \neg p$

Proof:
{{BeginTableau|\vdash \paren {p \implies \neg p} \implies \neg p}}
{{Premise|1|p \implies \neg p}}
{{Assumption|2|p}}
{{ModusPonens|3|1, 2|\neg p|1|2}}
{{NonContradiction|4|1, 2|2|3}}
{{Contradiction|5|1|\neg p|2|4}}
{{Implication|6||\paren {p \implies \neg p} \implies \neg p|1|5}}
{{EndTableau|qed}}
Theorem: Proof by Contradiction/Variant 3/Formulation 2

:$\vdash \paren {p \implies \neg p} \implies \neg p$

Proof:
{{BeginTableau|\vdash \paren {p \implies \neg p} \implies \neg p|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = \paren {p \lor p} \implies p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 1$
}}
{{TableauLine
 | n = 2
 | f = \paren {\neg p \lor \neg p} \implies \neg p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 1
 | c = $\neg p \, / \, p$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \implies \neg p} \implies \neg p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 2 \, (2)$
 | dep = 2
}}
{{EndTableau|qed}}
Theorem: Primitive of Function on Connected Domain

Let $f: D \to \C$ be a continuous complex function, where $D$ is a connected domain.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$f$ has a primitive.}}
{{item|(2):|For any two contours $C_1, C_2$ in $D$ with identical start points $z_1 \in D$ and end points $z_2 \in D$, we have:
:$\ds \int_{C_1} \map f z \rd z {{=}} \int_{C_2} \map f z \rd z$
}}
{{item|(3):|For all closed contours $C$ in $D$, we have:
:$\ds \oint_C \map f z \rd z {{=}} 0$
}}
{{end-itemize}}
If the conditions hold, we can choose any $z_0 \in D$ and define a primitive $F: D \to \C$ of $f$ by:
:$\ds \map F w = \int_{C_w} \map f z \rd z$
where $C_w$ is any contour in $D$ with start point $z_0$ and end point $w$.

Proof:
=== $(1)$ implies $(2)$ ===
If $F$ is a primitive of $f$, we have:
{{begin-eqn}}
{{eqn | l = \int_{C_1} \map f z \rd z 
      | r = \map F {z_2} - \map F {z_1}
      | c = Fundamental Theorem of Calculus for Contour Integrals
}}
{{eqn | r = \int_{C_2} \map f z \rd z 
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Upper Closure is Strict Upper Closure of Immediate Predecessor

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $b$ be the immediate successor element of $a$:
Then:
:$a^\succ = b^\succcurlyeq$
where:
:$a^\succ$ is the strict upper closure of $a$
:$b^\succcurlyeq$ is the upper closure of $b$.

Proof:
Let:
:$x \in a^\succ$
By the definition of strict upper closure:
:$a \prec x$
By the definition of total ordering:
:$x \prec b$ or $x \succcurlyeq b$
If $x \prec b$ then $a \prec x \prec b$, contradicting the premise.
Thus:
:$x \succcurlyeq b$
and so:
:$x \in b^\succcurlyeq$
By definition of subset:
:$a^\succ \subseteq b^\succcurlyeq$
Let:
:$x \in b^\succcurlyeq$
By the definition of upper closure:
:$b \preccurlyeq x$
Since $a \prec b$, Extended Transitivity shows that $a \prec x$.
Thus:
:$x \in a^\succ$
By definition of subset:
:$b^\succcurlyeq \subseteq a^\succ$
Therefore by definition of set equality:
:$a^\succ = b^\succcurlyeq$
{{qed}}
Category:Total Orderings
Category:Upper Closures
5euvbalimsdovq27rb54t80vcxj1hlf
Theorem: Proof by Contradiction/Sequent Form

:$\paren {p \vdash \bot} \vdash \neg p$

Proof:
{{BeginTableau|\paren {p \vdash \bot} \vdash \neg p}}
{{Premise      |1|p \vdash \bot}}
{{Assumption   |2|p}}
{{Contradiction|3|1|\neg p|2|2}}
{{EndTableau|qed}}
Category:Proof by Contradiction
4ukf0bn4xlan505yq1y2q3x5nvh59xg
Theorem: Left or Right Inverse of Matrix is Inverse

Let $\mathbf A, \mathbf B$ be square matrices of order $n$ over a commutative ring with unity $\struct {R, +, \circ}$.
Suppose that:
:$\mathbf A \mathbf B = \mathbf I_n$
where $\mathbf I_n$ is the unit matrix of order $n$.
Then $\mathbf A$ and $\mathbf B$ are nonsingular matrices, and furthermore:
:$\mathbf B = \mathbf A^{-1}$
where $\mathbf A^{-1}$ is the inverse of $\mathbf A$.

Proof:
Let $1_R$ denote the unity of $R$.
We have:
{{begin-eqn}}
{{eqn | l = 1_R
      | r = \map \det {\mathbf I_n}
      | c = Determinant of Unit Matrix
}}
{{eqn | r = \map \det {\mathbf A \mathbf B}
      | c = {{hypothesis}}
}}
{{eqn | r = \map \det {\mathbf A} \map \det {\mathbf B}
      | c = Determinant of Matrix Product
}}
{{end-eqn}} 
From Matrix is Nonsingular iff Determinant has Multiplicative Inverse, it follows that $\mathbf A$ and $\mathbf B$ are nonsingular.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf B
      | r = \mathbf I_n \mathbf B
      | c = Unit Matrix is Unity of Ring of Square Matrices
}}
{{eqn | r = \paren {\mathbf A^{-1} \mathbf A} \mathbf B
      | c = {{Defof|Inverse Matrix}}
}}
{{eqn | r = \mathbf A^{-1} \paren {\mathbf A \mathbf B}
      | c = Matrix Multiplication is Associative
}}
{{eqn | r = \mathbf A^{-1} \mathbf I_n
      | c = {{hypothesis}}
}}
{{eqn | r = \mathbf A^{-1}
      | c = Unit Matrix is Unity of Ring of Square Matrices
}}
{{end-eqn}}
{{qed}}
Theorem: Banach-Alaoglu Theorem

Let $X$ be a separable normed vector space.
Then the closed unit ball in its normed dual $X^*$ is sequentially compact with respect to the weak-$\ast$ topology.

Proof:
The aim of this proof is to show the following:
Given a bounded sequence in $X^*$, there exists a weakly convergent subsequence of that bounded sequence.
Let $\sequence {l_n}_{n \mathop \in \N}$ be a bounded sequence in $X^*$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a countable dense subset of $X$.
Choose subsequences $\N \supset \Lambda_1 \supset \Lambda_2 \supset \ldots$ such that:
:$\forall j \in \N: \map {l_k} {x_j} \to a_j =: \map l {x_j}$
as $k \to \infty$, $k \in \Lambda_j$.
{{explain|Why does $a_j$ exist?}}
Let $\Lambda$ be the diagonal sequence.
=== Lemma 1 ===
{{:Banach-Alaoglu Theorem/Lemma 1}}{{qed|lemma}}
=== Lemma 2 ===
{{:Banach-Alaoglu Theorem/Lemma 2}}{{qed|lemma}}
Theorem: Banach-Alaoglu Theorem

Let $X$ be a separable normed vector space.
Then the closed unit ball in its normed dual $X^*$ is sequentially compact with respect to the weak-$\ast$ topology.

Proof:
Let $X$ be a normed vector space.
Denote by $B$ the closed unit ball in $X$.
Let $X^*$ be the dual of $X$.
Denote by $B^*$ the closed unit ball in $X^*$.
Let:
:$\map \FF B = \closedint {-1} 1^B$ 
be the topological space of functions from $B$ to $\closedint {-1} 1$.
By Tychonoff's Theorem:
:$\map \FF B$ 
is compact with respect to the product topology.
We define the restriction map:
:$R: B^* \to \map \FF B$
by:
:$\forall \psi \in B^*: \map R \psi = \psi \restriction_B$
=== Lemma 3 ===
{{:Banach-Alaoglu Theorem/Lemma 3}}{{qed|lemma}}
=== Lemma 4 ===
{{:Banach-Alaoglu Theorem/Lemma 4}}{{qed|lemma}}
Thus by Lemma 4, $B^*$ in the weak* topology is homeomorphic with $R \sqbrk {B^*}$.
This is a closed set of $\map \FF B$ (by Lemma 3) and thus compact.
By the Eberlein-Šmulian Theorem, this is sequentially compact.
{{explain|Exactly what the Eberlein-Šmulian Theorem that results in the above conclusion}}
{{mistake|No, this is wrong. Eberlein-Šmulian Theorem is not sufficient. Edit: I think Banach-Alaoglu ends up getting used in the proof of Eberlein-Šmulian anyway...}}
{{finish|We need to use the metrization to conclude sequential compactness.}}
Theorem: Banach-Alaoglu Theorem

Let $X$ be a separable normed vector space.
Then the closed unit ball in its normed dual $X^*$ is sequentially compact with respect to the weak-$\ast$ topology.

Proof:
Let $B_{X^\ast}$ be the closed unit ball in $X^\ast$. 
Let $w^\ast$ be the weak-$\ast$ topology on $X^\ast$. 
From the definition of the norm of a bounded linear functional, we have: 
:$B_{X^\ast} = \set {f : X \to \GF : \cmod {\map f x} \le \norm x \text { and } f \text { is linear} }$
For each $x \in X$, let: 
:$K_x = \set {\lambda \in \GF : \cmod \lambda \le \norm x}$ 
Let: 
:$\ds K = \prod_{x \mathop \in X} K_x$ 
equipped with the product topology. 
Then if $f \in K$ and $x \in X$ we have $\map f x \in K_x$ {{iff}} $\cmod {\map f x} \le \norm x$. 
Then: 
:$B_{X^\ast} = \set {f \in K : f \text { is linear} }$
Let $\pr_x : K \to \GF$ denote the projection onto the $x$th factor, that is: 
:$\map {\pr_x} f = \map f x$ 
for each $f \in K$.
From the definition of the product topology, the product topology on $K$ is the initial topology induced by $\set {\pr_x : x \in X}$. 
From Subspace Topology on Initial Topology is Initial Topology on Restrictions, the subspace topology on $B_{X^\ast}$ inherited by $K$ is the initial topology on $B_{X^\ast}$ induced by $\set {\pr_x \restriction_{B_{X^\ast} } : x \in X}$.
Applying Subspace Topology on Initial Topology is Initial Topology on Restrictions to $\struct {X^\ast, w^\ast}$, this is precisely the subspace topology on $B_{X^\ast}$ inherited by the weak-$\ast$ topology on $X^\ast$. 
From Tychonoff's Theorem, $K$ is compact. 
From Closed Subspace of Compact Space is Compact, it suffices to show that $B_{X^\ast}$ is closed in $\struct {K$.
We may now write: 
{{begin-eqn}}
{{eqn	| l = B_{X^\ast}
		| r = \set {f \in K : \lambda \map f x + \mu \map f y = \map f {\lambda x + \mu y} \text { for all } x, y \in X, \, \lambda, \mu \in \GF}
}}
{{eqn	| r = \set {f \in K : \map {\paren {\lambda \pr_x + \mu \pr_y - \pr_{\lambda x + \mu y} } } f = 0 \text { for all } x, y \in X, \, \lambda, \mu \in \GF}
}}
{{eqn	| r = \bigcap_{x, y \in X, \, \lambda, \mu \in \GF} \paren {\lambda \pr_x + \mu \pr_y - \pr_{\lambda x + \mu y} }^{-1} \sqbrk {\set 0}
}}
{{end-eqn}}
From Linear Combination of Continuous Functions valued in Topological Vector Space is Continuous: 
:$\lambda \pr_x + \mu \pr_y - \pr_{\lambda x + \mu y}$ is continuous for each $x, y \in X$ and $\lambda, \mu \in \GF$.
From Continuity Defined from Closed Sets, we have that: 
:$\paren {\lambda \pr_x + \mu \pr_y - \pr_{\lambda x + \mu y} }^{-1} \sqbrk {\set 0}$ is closed in $K$. 
Since the intersection of closed sets is closed, we have that: 
:$\ds \bigcap_{x, y \in X, \, \lambda, \mu \in \GF} \paren {\lambda \pr_x + \mu \pr_y - \pr_{\lambda x + \mu y} }^{-1} \sqbrk {\set 0}$ is closed in $K$.
So $\struct {B_{X^\ast}, w^\ast}$ is closed in $K$.
From Closed Subspace of Compact Space is Compact, $\struct {B_{X^\ast}, w^\ast}$ is compact.
{{qed}}
Theorem: Empty Product is Terminal Object

Let $\mathbf C$ be a metacategory.
Suppose $\mathbf C$ admits a product $\prod \O$ for the empty set.
Then $\prod \O$ is a terminal object of $\mathbf C$.

Proof:
By definition, $\prod \O$ is the limit of the empty subcategory $\mathbf 0$ of $\mathbf C$.
The result follows from Terminal Object as Limit.
{{qed}}
Category:Limits and Colimits
Category:Products (Category Theory)
2nfoe9f4wxtj0u65bqnab4a3qe0i0aa
Theorem: Unary Product for Object is Itself

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Then $\ds \prod \set C = C$, where $\ds \prod$ denotes product.

Proof:
Follows directly from Limit of Singleton.
{{qed}}
Category:Objects (Category Theory)
Category:Category Theory
0aw7ydwpy1bhtsooxhhie3203zwv2ok
Theorem: Principle of Non-Contradiction/Sequent Form/Formulation 1

:$p, \neg p \vdash \bot$

Proof:
{{BeginTableau|p, \neg p \vdash \bot}}
{{Premise|1|p}}
{{Premise|2|\neg p}}
{{NonContradiction|3|1, 2|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Principle of Non-Contradiction/Sequent Form/Formulation 1

:$p, \neg p \vdash \bot$

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin {array} {|cccc||c|} \hline
p & \land & \neg & p & \bot \\
\hline
\F & \F & \T & \F & \F \\
\T & \F & \F & \T & \F \\
\hline
\end {array}$</nowiki>
As can be seen by inspection, the truth value of the main connective, that is $\land$, is $F$ for each boolean interpretation for $p$.
{{qed}}
Theorem: Vector Cross Product is Orthogonal to Factors

Let $\mathbf a$ and $\mathbf b$ be vectors in the real Euclidean space $\R^3$.
Let $\mathbf a \times \mathbf b$ denote the vector cross product.
Then:
{{begin-itemize}}
{{item|(1):|$\mathbf a$ and $\mathbf a \times \mathbf b$ are orthogonal.}}
{{item|(2):|$\mathbf b$ and $\mathbf a \times \mathbf b$ are orthogonal.}}
{{end-itemize}}

Proof:
Let $\mathbf a = \begin {bmatrix} a_1 \\ a_2 \\ a_3 \end {bmatrix}$, and $\mathbf b = \begin {bmatrix} b_1 \\ b_2 \\ b_3 \end {bmatrix}$.
Then the dot product of $\mathbf a$ and $\mathbf a \times \mathbf b$ is:
{{begin-eqn}}
{{eqn | l = \mathbf a \cdot \paren {\mathbf a \times \mathbf b}
      | r = a_1 \paren {a_2 b_3 - a_3 b_2} + a_2 \paren {a_3 b_1 - a_1 b_3} + a_3 \paren {a_1 b_2 - a_2 b_1}
      | c = {{Defof|Dot Product}} and {{Defof|Vector Cross Product}}
}}
{{eqn | r = a_1 a_2 b_3 - a_1 a_3 b_2 + a_2 a_3 b_1 - a_1 a_2 b_3 + a_1 a_3 b_2 - a_2 a_3 b_1
}}
{{eqn | r = 0
}}
{{end-eqn}}
Since the dot product is equal to zero, the vectors $\mathbf a$ and $\mathbf a \times \mathbf b$ are orthogonal by definition.
Similarly, $\mathbf b$ and $\mathbf a \times \mathbf b$ are orthogonal:
{{begin-eqn}}
{{eqn | l = \mathbf b \cdot \paren {\mathbf a \times \mathbf b}
      | r = b_1 \paren {a_2 b_3 - a_3 b_2} + b_2 \paren {a_3 b_1 - a_1 b_3} + b_3 \paren {a_1 b_2 - a_2 b_1}
}}
{{eqn | r = a_2 b_1 b_3 - a_3 b_1 b_2 + a_3 b_1 b_2 - a_1 b_2 b_3 + a_1 b_2 b_3 - a_2 b_1 b_3
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Squeeze Theorem/Sequences/Metric Spaces

Let $M = \struct {S, d}$ be a metric space or pseudometric space.
Let $p \in S$.
Let $\sequence {r_n}$ be a null sequence in $\R$.
Let $\sequence {x_n}$ be a sequence in $S$ such that:
:$\forall n \in \N: \map d {p, x_n} \le r_n$.
Then $\sequence {x_n}$ converges to $p$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = \map d {p, x_n}
      | o = \le
      | r = r_n
      | c = {{hypothesis}}
}}
{{eqn | q = \forall n \in \N
      | l = r_n
      | o = \le
      | r = \size {r_n}
      | c = Negative of Absolute Value
}}
{{eqn | q = \forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N
      | lo= n > N \implies
      | l = \size {r_n}
      | o = <
      | r = \epsilon
      | c = {{Defof|Null Sequence|subdef = Real Numbers}}
}}
{{eqn | ll= \leadsto
      | q = \forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N
      | lo= n > N \implies
      | l = \map d {p, x_n}
      | o = <
      | r = \epsilon
      | c = Extended Transitivity
}}
{{end-eqn}}
Thus $\sequence {x_n}$ converges to $p$.
{{qed}}
Category:Metric Spaces
Category:Limits of Sequences
p6dnyy4qx6bro8bnw386hc8t3evakud
Theorem: Squeeze Theorem/Sequences/Linearly Ordered Space

Let $\struct {S, \le, \tau}$ be a linearly ordered space.
Let $\sequence {x_n}$, $\sequence {y_n}$, and $\sequence {z_n}$ be sequences in $S$.
Let $p \in S$.
Let $\sequence {x_n}$ and $\sequence {z_n}$ both converge to $p$.
Let $\forall n \in \N: x_n \le y_n \le z_n$.
Then $\sequence {y_n}$ converges to $p$.

Proof:
Let $m \in S$ and $m < p$.
Then $\sequence {x_n}$ eventually succeeds $m$.
Thus by Extended Transitivity, $\sequence {y_n}$ eventually succeeds $m$.
A similar argument using $\sequence {z_n}$ proves the dual statement.
Thus $\sequence {y_n}$ is eventually in each ray containing $p$, so it converges to $p$.
{{qed}}
Category:Linearly Ordered Spaces
Category:Limits of Sequences
abobfdi4j5q1wpypvokakmqhp9r2xaa
Theorem: Squeeze Theorem for Filter Bases

Let $\struct {S, \le, \tau}$ be a linearly ordered space.
Let $F_1$, $F_2$, and $F_3$ be filter bases in $S$.
Let:
:$\forall T \in F_1: \exists M \in F_2: \forall x \in M: \exists y \in T: y \le x$
That is:
:for each $T \in F_1$, $F_2$ has an element $M$ such that all elements of $M$ succeed some element of $T$.
Similarly, let:
:$\forall U \in F_3: \exists N \in F_2: \forall x \in N: \exists y \in U: x \le y$
That is:
:for each $U \in F_3$, $F_2$ has an element $N$ such that all elements of $N$ precede some element of $U$.
Let $F_1$ and $F_3$ each converge to a point $p \in S$.
Then $F_2$ converges to $p$.

Proof:
Let $q \in S$ such that $q < p$.
We will show that $F_2$ has an element which is a subset of $q^\ge$.
{{explain|$q^\ge$ is the upper closure in what set?}}
Since $F_1$ converges to $p$, it has an element:
:$A \subseteq q^\ge$.
Thus there is an element $k$ in $A$ and an element $M$ in $F_2$ such that all elements of $M$ succeed $k$.
Then by Extended Transitivity:
:$M \subseteq q^\ge$
A similar argument using $F_3$ proves the dual statement.
Thus $F_2$ converges to $p$.
{{explain}}
{{qed}}
Category:Filter Theory
Category:Linearly Ordered Spaces
Category:Convergence
n82lw7w0hpqz0cmtvu0weuu1l4talfi
Theorem: Non-Zero Vectors are Orthogonal iff Perpendicular

Let $\mathbf u$, $\mathbf v$ be non-zero vectors in the real Euclidean space $\R^n$.
Then $\mathbf u$ and $\mathbf v$ are orthogonal {{iff}} they are perpendicular.

Proof:
=== Necessary Condition ===
When $\theta$ denotes the angle between $\mathbf u$ and $\mathbf v$ measured in radians, we have:
{{begin-eqn}}
{{eqn | l = 0
      | r = \mathbf u \cdot \mathbf v
      | c = {{Defof|Orthogonal Vectors}}
}}
{{eqn | r = \norm {\mathbf u} \norm {\mathbf v} \cos \theta
      | c = Cosine Formula for Dot Product
}}
{{end-eqn}}
where $\norm {\,\cdot\,}$ denotes the Euclidean norm.
As $\mathbf u, \mathbf v$ are non-zero vectors, it follows from the norm axiom of positive definiteness that $\norm {\mathbf u} \ne 0$, and $\norm {\mathbf v} \ne 0$.
Then $\cos \theta = 0$.
It follows from Zeroes of Sine and Cosine that $\theta = \dfrac \pi 2$, given that $\theta \in \closedint 0 \pi$ by the convention of the definition of angle between vectors.
Then $\mathbf u$ and $\mathbf v$ are perpendicular by the measurement of a right angle.
{{qed|lemma}}
Theorem: Exponential Function is Continuous/Complex

:$\forall z_0 \in \C: \ds \lim_{z \mathop \to z_0} \exp z = \exp z_0$

Proof:
This proof depends on the differential equation definition of the exponential function.
The result follows from Complex-Differentiable Function is Continuous.
{{qed}}
Category:Exponential Function is Continuous
nxshz8om78e0hbqwlg95tfzbpc71tr7