avewright/proofwiki-math huggingface dataset:
Theorem: Relation Compatible with Group Operation is Reflexive or Antireflexive

Let $\struct {G, \circ}$ be a group.
Let $\RR$ be a relation on $G$ that is compatible with $\circ$.
Then $\RR$ is reflexive or antireflexive.

Proof:
Suppose that $\RR$ is not antireflexive.
Then there is some $x \in G$ such that $x \mathrel \RR x$.
Let $y \in G$.
Then by the definition of compatibility:
:$\paren {x \circ \paren {x^{-1} \circ y} } \mathrel \RR \paren {x \circ \paren {x^{-1} \circ y} }$
By {{Group-axiom|1}} and {{Group-axiom|3}}:
:$y \mathrel \RR y$
Since this holds for arbitrary $y$, $\RR$ is reflexive.
Thus $\RR$ is either reflexive or antireflexive.
{{qed}}
{{explain|While the above demonstrates that if such a relation is not antireflexive it must be reflexive, it does not approach the task of demonstrating that such a relation can actually *be* antireflexive.}}
Category:Relations Compatible with Group Operation
Category:Reflexive Relations
Category:Antireflexive Relations
jv9nw3bfs1buqelm8toi9vqaulxbkcv
Theorem: Linearly Ordered Space on Order-Convex Subset is Subspace Topology

Let $\struct {S, \preceq,\tau}$ be a linearly ordered space.
Let $A \subseteq S$ be a order-convex set in $S$.
Let $\upsilon$ be the order topology on $A$.
Let $\tau'$ be the $\tau$-relative subspace topology on $A$.
Then $\upsilon = \tau'$.

Proof:
{{improve|Reword so as to be less wordy. Add pictures so as to be easier to visualize.}}
By the definition of the order topology, the sets of open rays in $\struct {S, \preceq}$ and $\struct {A, \preceq}$ form sub-bases for $\tau$ and $\upsilon$, respectively.
By Sub-Basis for Topological Subspace, we need only show that the set of open rays in $\struct {S, \preceq}$ induces a subbase for $\upsilon$.
Specifically, we will show that each open ray in $A$ is the intersection of $A$ with an open ray in $S$, and we will show that the intersection of any open ray in $S$ with $A$ is either an open ray in $A$, the empty set, or $A$.
From Strict Lower Closure is Dual to Strict Upper Closure and duality principle, we need to show this only for the upward-pointing rays.
For each $p \in S$, let $p^{\succ S}$ be the strict upper closure of $p$ in $S$.
For each $p \in A$, let $p^{\succ A}$ be the strict upper closure of $p$ in $A$.
Let $p \in A$.
Then by Strict Upper Closure in Restricted Ordering:
:$p^{\succ A} = A \cap p^{\succ S}$
Let $q \in S$.
If $q \in A$, then $A \cap q^{\succ S} = q^{\succ A}$, so $A \cap q^{\succ S}$ is an open ray in $A$.
Suppose instead that $q \notin A$.
If $A \cap q^{\succ S} = \O$, the proof is complete.
Otherwise, $A \cap q^{\succ S}$ must have some element $x$.
{{AimForCont}} there is a $y \in A \setminus \paren {A \cap q^{\succ S} } = A \cap q^{\preceq S}$.
Then since $q \notin A$, it follows that $y \prec q$.
Thus $y \prec q \prec x$, $y, x \in A$, and $q \notin A$, contradicting the fact that $A$ is order-convex.
Thus $A \cap q^{\succ S} = A$.
{{qed}}
Category:Linearly Ordered Spaces
Category:Topological Subspaces
0gvhoyfqqvtya01fbwq7exf1c1cpzk4
Theorem: Exponential Function is Continuous/Real Numbers

The real exponential function is continuous.
That is:
:$\forall x_0 \in \R: \ds \lim_{x \mathop \to x_0} \exp x = \exp x_0$

Proof:
This proof depends on the limit definition of the exponential function.
Let:
:$\ds \exp x = \lim_{n \mathop \to \infty} \paren {1 + \dfrac x n}^n$
Fix $x_0 \in \R$.
Consider $I := \closedint {x_0 - 1} {x_0 + 1}$.
From Closed Bounded Subset of Real Numbers is Compact, $I$ is compact.
From Exponential Sequence is Uniformly Convergent on Compact Sets:
:$\paren {1 + \dfrac x n}^n$ is uniformly convergent on $I$.
By the Uniform Limit Theorem:
:$\ds \lim_{n \mathop \to \infty} \paren {1 + \dfrac x n}^n = \exp x$
is continuous on $I$.
In particular, $\exp x$ is continuous at $x_0$.
{{qed}}
Theorem: Exponential Function is Continuous/Real Numbers

The real exponential function is continuous.
That is:
:$\forall x_0 \in \R: \ds \lim_{x \mathop \to x_0} \exp x = \exp x_0$

Proof:
This proof depends on the definition of the exponential function as the function inverse of the natural logarithm.
From Logarithm is Strictly Increasing, $\ln$ is strictly monotone on $\R_{>0}$.
From Real Natural Logarithm Function is Continuous, $\ln$ is continuous on $\R_{>0}$
Thus, from the Continuous Inverse Theorem, $\exp := \ln^{-1}$ is continuous.
{{qed}}
Theorem: Exponential Function is Continuous/Real Numbers

The real exponential function is continuous.
That is:
:$\forall x_0 \in \R: \ds \lim_{x \mathop \to x_0} \exp x = \exp x_0$

Proof:
This proof depends on the differential equation definition of the exponential function.
The result follows from Differentiable Function is Continuous.
{{qed}}
Theorem: Exponential Function is Continuous/Real Numbers

The real exponential function is continuous.
That is:
:$\forall x_0 \in \R: \ds \lim_{x \mathop \to x_0} \exp x = \exp x_0$

Proof:
This proof depends on the continuous extension definition of the exponential function.
Let $\exp$ be the unique continuous extension of $e^x$ from $\Q$ to $\R$.
By definition, $\exp$ is continuous.
Hence the result.
{{qed}}
Theorem: Exponential Function is Continuous/Real Numbers

The real exponential function is continuous.
That is:
:$\forall x_0 \in \R: \ds \lim_{x \mathop \to x_0} \exp x = \exp x_0$

Proof:
This proof depends on the series definition of $\exp$.
That is, let:
:$\ds \exp x = \sum_{k \mathop = 0}^ \infty \frac {x^k} {k!}$
From Series of Power over Factorial Converges, the radius of convergence of $\exp$ is $\infty$.
Thus, from Power Series Converges to Continuous Function, $\exp$ is continuous on $\R$.
{{qed}}
Theorem: Edge of Tree is Bridge

Let $T$ be a tree.
Let $e$ be an edge of $T$.
Then $e$ is a bridge of $T$.

Proof:
From Condition for Edge to be Bridge, $e$ is a bridge {{iff}} $e$ does not lie on any circuit.
Since $T$ is a tree, there are no circuits in $T$.
The result follows.
{{qed}}
Category:Tree Theory
2gv9ezkowkeum6iuxybx22zdv45vg9z
Theorem: Sub-Basis for Topological Subspace

Let $\struct {X, \tau}$ be a topological space.
Let $K$ be a sub-basis for $\tau$.
Let $\struct {S, \tau'}$ be a subspace of $\struct {X, \tau}$.
Let $K' = \set {U \cap S: U \in K}$.
That is, $K'$ consists of the $\tau'$-open sets in $S$ corresponding to elements of $K$.
Then $K'$ is a sub-basis for $\tau'$.

Proof:
Let $B$ be the basis for $\tau$ generated by $K$.
By Basis for Topological Subspace, $B$ generates a basis, $B'$, for $\tau'$.
We will show that $K'$ generates $B'$.
Let $V' \in B'$.
Then for some $V \in B$:
:$V' = S \cap V$
By the definition of a sub-basis, there is a finite subset $K_V$ of $K$ such that:
:$\ds V = \bigcap K_V$
Let $K_V' = \set {S \cap U: U \in K_V}$.
Then:
:$\ds V' = S \cap V = S \cap \bigcap K_V$
so:
:$\ds V' = \bigcap_{P \mathop \in K_V} \paren {S \cap P} = \bigcap K_V'$
Thus $B'$ is generated by $K'$.
{{qed}}
Category:Topological Bases
Category:Topological Subspaces
ktf8gr6vwf3yzkl4w459yw4q4kxx845
Theorem: Modus Ponendo Ponens/Variant 2

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

Proof:
{{BeginTableau|\vdash p \implies \paren {\paren {p \implies q} \implies q} }}
{{Assumption|1|p}}
{{Assumption|2|p \implies q}}
{{ModusPonens|3|1, 2|q|2|1}}
{{Implication|4|1|\paren {p \implies q} \implies q|2|3}}
{{Implication|5||p \implies \paren {\paren {p \implies q} \implies q}|1|4}}
{{EndTableau|qed}}
Theorem: Modus Ponendo Ponens/Variant 2

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

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|c|c|ccccc|} \hline
p & \implies & ((p & \implies & q) & \implies & q)\\
\hline
\F & \T & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen by inspection, the main connective is true throughout.
{{qed}}
Theorem: Rule of Commutation/Conjunction

Conjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Conjunction/Formulation 2}}

Proof:
{{BeginTableau|p \land q \vdash q \land p}}
{{Premise|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q|1|2}}
{{Conjunction|4|1|q \land p|3|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|q \land p \vdash p \land q}}
{{Premise|1|q \land p}}
{{Simplification|2|1|q|1|1}}
{{Simplification|3|1|p|1|2}}
{{Conjunction|4|1|p \land q|3|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Conjunction

Conjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Conjunction/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||ccc|} \hline
p & \land & q & q & \land & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \T & \T & \F & \F \\
\T & \F & \F & \F & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Commutation/Conjunction

Conjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Conjunction/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \land q} \iff \paren {q \land p} }}
{{Assumption |1|p \land q}}
{{Commutation|2|1|q \land p|1|Conjunction}}
{{Implication|3||\paren {p \land q} \implies \paren {q \land p}|1|2}}
{{Assumption |4|q \land p}}
{{Commutation|5|4|p \land q|4|Conjunction}}
{{Implication|6||\paren {q \land p} \implies \paren {p \land q}|4|5}}
{{BiconditionalIntro|7||\paren {p \land q} \iff \paren {q \land p}|3|6}}
{{EndTableau|qed}}
Theorem: Rule of Commutation/Disjunction

Disjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Disjunction/Formulation 2}}

Proof:
{{BeginTableau|p \lor q \vdash q \lor p}}
{{Premise|1|p \lor q}}
{{Assumption|2|p}}
{{Addition|3|2|q \lor p|2|2}}
{{Assumption|4|p}}
{{Addition|5|4|q \lor p|4|1}}
{{ProofByCases|6|1|q \lor p|1|2|3|4|5}}
{{EndTableau}}
{{qed}}
{{BeginTableau|q \lor p \vdash p \lor q}}
{{Premise|1|q \lor p}}
{{Assumption|2|q}}
{{Addition|3|2|p \lor q|2|2}}
{{Assumption|4|p}}
{{Addition|5|4|p \lor q|4|1}}
{{ProofByCases|6|1|p \lor q|1|2|3|4|5}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Disjunction

Disjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Disjunction/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in both cases, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc||ccc|} \hline
p & \lor & q & q & \lor & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Commutation/Disjunction

Disjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Disjunction/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \lor q} \iff \paren {q \lor p} }}
{{Assumption|1|p \lor q}}
{{Commutation|2|1|q \lor p|1|Disjunction}}
{{Implication|3||\paren {p \lor q} \implies \paren {q \lor p}|1|2}}
{{Assumption|4|q \lor p}}
{{Commutation|5|4|p \lor q|4|Disjunction}}
{{Implication|6||\paren {q \lor p} \implies \paren {p \lor q}|4|5}}
{{BiconditionalIntro|7||\paren {p \lor q} \iff \paren {q \lor p}|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Disjunction

Disjunction is commutative:
=== Formulation 1 ===
{{:Rule of Commutation/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Commutation/Disjunction/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc|c|ccc|} \hline
(p & \lor & q) & \iff & (q & \lor & p) \\
\hline
\F & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \F \\
\T & \T & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Factor Principles/Conjunction on Right/Formulation 1

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

Proof:
{{BeginTableau|p \implies q \vdash \paren {p \land r} \implies \paren {q \land r} }}
{{Premise|1|p \implies q}}
{{IdentityLaw|2||r \implies r|(None)|This is a theorem so depends on nothing}}
{{Conjunction|3|1|\paren {p \implies q} \land \paren {r \implies r}|1|2}}
{{SequentIntro|4|1|\paren {p \land r} \implies \paren {q \land r}|3|Praeclarum Theorema}}
{{EndTableau|qed}}
Theorem: Factor Principles/Conjunction on Right/Formulation 1

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

Proof:
{{BeginTableau|p \implies q \vdash \paren {p \land r} \implies \paren {q \land r} }}
{{Premise       |1|p \implies q}}
{{Assumption    |2|p \land r}}
{{Simplification|3|2|p|2|1}}
{{ModusPonens   |4|1, 2|q|1|3}}
{{Simplification|5|2|r|2|2}}
{{Conjunction   |6|1, 2|q \land r|4|5}}
{{Implication   |7|1|\paren {p \land r} \implies \paren {q \land r}|2|6}}
{{EndTableau|qed}}
Theorem: Factor Principles/Conjunction on Right/Formulation 1

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

Proof:
Proof by Truth Table:
$\begin{array}{|ccc||ccccccccccc|}
\hline
p & q & r & (p & \implies & q) & \implies & ((p & \land & r) & \implies & (q & \land & r)) \\
\hline
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\T & \T & \F & \T & \T & \T & \T & \T & \F & \F & \T & \T & \F & \F \\
\T & \F & \T & \T & \F & \F & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \F & \F & \T & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\F & \T & \F & \F & \T & \T & \T & \F & \F & \F & \T & \T & \F & \F \\
\F & \F & \T & \F & \T & \F & \T & \F & \F & \T & \T & \F & \F & \T \\
\F & \F & \F & \F & \T & \F & \T & \F & \F & \F & \T & \F & \F & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Interior of Convex Angle is Convex Set

Let $\mathbf v, \mathbf w$ be two non-zero vectors in $\R^2$, and let $p$ be a point in $\R^2$.
Suppose that the angle between $\mathbf v$ and $\mathbf w$ is a convex angle.
Then the set 
:$U = \set {p + s t \mathbf v + \paren {1 - s} t \mathbf w : s \in \openint 0 1, t \in \R_{>0} }$
is a convex set.

Proof:
Let $p_1, p_2 \in U$.
Then for $i \in \set {1, 2}$, $p_i = p + s_i t_i \mathbf v + \paren {1 - s_i} t_i \mathbf w$ for some $s_i \in \openint 0 1, t_i \in \R_{>0}$.
:File:InteriorOfConvexAngle.png
{{WLOG}}, assume that $t_1 \le t_2$.
Suppose that $q \in \R^2$ lies on the line segment joining $p_1$ and $p_2$, so:
{{begin-eqn}}
{{eqn | l = q
      | r = p + s_1 t_1 \mathbf v + \paren {1 - s_1} t_1 \mathbf w + s \paren {p + s_2 t_2 \mathbf v + \paren {1 - s_2} t_2 \mathbf w - p - s_1 t_1 \mathbf v - \paren {1 - s_1} t_1 \mathbf w}
      | c = for some $s \in \openint 0 1$
}}
{{eqn | r = p + \paren {\paren {1 - s} s_1 t_1 + s s_2 t_2} \mathbf v + \paren {\paren {1 - s} \paren {1 - s_1} t_1 + s \paren {1 - s_2} t_2} \mathbf w
}}
{{eqn | r = p + \dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r r \mathbf v + \dfrac {t_1 + s t_2 - s t_1 - \paren {1 - s} s_1 t_1 - s s_2 t_2} r r \mathbf w
      | c = where $r = t_1 + s \paren {t_2 - t_1}$
}}
{{eqn | r = p + \dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r r \mathbf v + \paren {1 - \dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r} r \mathbf w
}}
{{end-eqn}}
As $t_1 \le t_2$, it follows that $r \in \R_{>0}$.
We have:
:$\dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r > 0$
and so:
{{begin-eqn}}
{{eqn | l = 1 - \dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r
      | r = \dfrac {\paren {1 - s} \paren {1 - s_1} t_1 + s \paren {1 - s_2} t_2} r
}}
{{eqn | o = >
      | r = 0
}}
{{end-eqn}}
It follows that:
:$\dfrac {\paren {1 - s} s_1 t_1 + s s_2 t_2} r \in \openint 0 1$
Then $q \in U$.
It follows by definition that $U$ is convex.
{{qed}}
Category:Vector Spaces
Category:Convex Sets (Vector Spaces)
esd80rq01ifxnth1s0a9i9acuqapqyw
Theorem: Factor Principles/Conjunction on Left/Formulation 1

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

Proof:
{{BeginTableau|p \implies q \vdash \paren {r \land p} \implies \paren {r \land q} }}
{{Premise|1|p \implies q}}
{{IdentityLaw|2||r \implies r|(None)|This is a theorem so depends on nothing}}
{{Conjunction|3|1|\paren {r \implies r} \land \paren {p \implies q}|2|1}}
{{SequentIntro|4|1|\paren {r \land p} \implies \paren {r \land q}|3|Praeclarum Theorema}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Conjunction on Left/Formulation 1

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

Proof:
{{BeginTableau|p \implies q \vdash \paren {r \land p} \implies \paren {r \land q} }}
{{Premise|1|p \implies q}}
{{Assumption|2|r \land p}}
{{Simplification|3|2|p|2|2}}
{{ModusPonens|4|1, 2|q|1|3}}
{{Simplification|5|2|r|2|1}}
{{Conjunction|6|1, 2|r \land q|5|4}}
{{Implication|7|1|\paren {r \land p} \implies \paren {r \land q}|2|6}}
{{EndTableau|qed}}
Theorem: Factor Principles/Conjunction on Left/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \implies \paren {\paren {r \land p} \implies \paren {r \land q} } }}
{{Assumption|1|p \implies q}}
{{Assumption|2|r \land p}}
{{Simplification|3|2|p|2|2}}
{{ModusPonens|4|1, 2|q|1|3}}
{{Simplification|5|2|r|2|1}}
{{Conjunction|6|1, 2|r \land q|5|4}}
{{Implication|7|1|\paren {r \land p} \implies \paren {r \land q}|2|6}}
{{Implication|8|1|\paren {p \implies q} \implies \paren {\paren {r \land p} \implies \paren {r \land q} }|1|7}}
{{EndTableau|qed}}
Theorem: Triangle is Convex Set

The interior of a triangle embedded in $\R^2$ is a convex set.

Proof:
Denote the triangle as $\triangle$, and the interior of the boundary of $\triangle$ as $\Int \triangle$.
From Boundary of Polygon is Jordan Curve, it follows that the boundary of $\triangle$ is equal to the image of a Jordan curve, so $\Int \triangle$ is well-defined.
Denote the vertices of $\triangle$ as $A_1, A_2, A_3$.
For $i \in \set {1, 2, 3}$, put $j = i \bmod 3 + 1$, $k = \paren {i + 1} \bmod 3 + 1$, and:
:$U_i = \set {A_i + s t \paren {A_j - A_i} + \paren {1 - s} t \paren {A_k - A_i}: s \in \openint 0 1, t \in \R_{>0} }$
Suppose that the angle $\angle A_i$ between $A_j - A_i$ and $A_k - A_i$ is non-convex.
As $\angle A_i$ is an internal angle in $\triangle$, it follows from definition of polygon that $\angle A_i$ cannot be zero or straight.
Then $\angle A_i$ is larger than a straight angle, which is impossible by Sum of Angles of Triangle Equals Two Right Angles.
It follows that $\angle A_i$ is convex.
From Characterization of Interior of Triangle, it follows that:
:$\ds \Int \triangle = \bigcap_{i \mathop = 1}^3 U_i$
From Interior of Convex Angle is Convex Set, it follows for $i \in \set {1, 2, 3}$ that $U_i$ is a convex set.
The result now follows from Intersection of Convex Sets is Convex Set (Vector Spaces).
{{qed}}
Category:Convex Sets (Vector Spaces)
c8ffcvf8t2ubsf453ip017qtjlczahq
Theorem: Norm of Vector Cross Product

Let $\mathbf a$ and $\mathbf b$ be vectors in the real Euclidean space $\R^3$.
Let $\times$ denote the vector cross product.
Then:
:$\norm {\mathbf a \times \mathbf b} = \norm {\mathbf a} \norm {\mathbf b} \size {\sin \theta}$
where $\theta$ is the angle between $\mathbf a$ and $\mathbf b$, or an arbitrary number if $\mathbf a$ or $\mathbf b$ is the zero vector.
{{explain|link to $\norm {\mathbf a}$ etc. defining what it means}}

Proof:
Suppose either $\mathbf a$ or $\mathbf b$ is the zero vector.
Then by {{NormAxiomVector|1}}:
:$\norm {\mathbf a} = 0$
or:
:$\norm {\mathbf b} = 0$
By calculation, it follows that $\mathbf a \times \mathbf b$ is also the zero vector.
Hence:
:$\norm {\mathbf a \times \mathbf b} = 0$
and equality holds.
Now suppose that both $\mathbf a$ or $\mathbf b$ are non-zero vectors.
We have:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf a \times \mathbf b}^2
      | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 - \paren {\mathbf a \cdot \mathbf b}^2
      | c = Square of Norm of Vector Cross Product
}}
{{eqn | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 - \norm {\mathbf a}^2 \norm {\mathbf b}^2 \cos^2 \theta 
      | c = Cosine Formula for Dot Product
}}
{{eqn | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 \paren{1 - \cos^2 \theta}
}}
{{eqn | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 \sin^2 \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll = \leadstoandfrom 
      | l = \norm {\mathbf a \times \mathbf b}
      | r = \norm {\mathbf a} \norm {\mathbf b} \size{\sin \theta}
      | c = taking the square root of both sides of the equality
}}
{{end-eqn}}
{{qed}}
Theorem: Subset Relation is Compatible with Subset Product/Corollary 1

Let $A, B, C, D \in \powerset S$.
Let $A \subseteq B$ and $C \subseteq D$.
Then:
:$A \circ_\PP C \subseteq B \circ_\PP D$

Proof:
By Subset Relation is Compatible with Subset Product, $\subseteq$ is compatible with $\circ_\PP$.
By Subset Relation is Transitive, $\subseteq$ is transitive.
Thus the theorem holds by Operating on Transitive Relationships Compatible with Operation.
{{qed}}
Category:Subset Products
Category:Compatible Relations
9ik95egri7v1sf47jv4bjk5cu4lamz5
Theorem: Subset Relation is Compatible with Subset Product/Corollary 2

Let $A, B \subseteq S$.
Let $A \subseteq B$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = x \circ A
      | o = \subseteq
      | r = x \circ B
}}
{{eqn | l = A \circ x
      | o = \subseteq
      | r = B \circ x
}}
{{end-eqn}}

Proof:
This follows from Subset Relation is Compatible with Subset Product and the definition of the subset product with a singleton.
{{qed}}
Category:Subset Products
axp9ujgrok4hgprkv48upqjov76lvmf
Theorem: Equivalence of Definitions of Normal Subset/1 iff 2

Let $\struct {G, \circ}$ be a group.
Let $S$ be a subset of $G$.
Then Normal Subset/Definition 1 is equivalent to Normal Subset/Definition 2.
That is, the following three statements are equivalent:
:$(1): \quad \forall g \in G: g \circ S = S \circ g$
:$(2): \quad \forall g \in G: g \circ S \circ g^{-1} = S$
:$(3): \quad \forall g \in G: g^{-1} \circ S \circ g = S$

Proof:
Let $e$ be the identity of $G$.
First note that:
:$(4): \quad \paren {\forall g \in G: g \circ S \circ g^{-1} = S} \iff \paren {\forall g \in G: g^{-1} \circ S \circ g = S}$
which is shown by, for example, setting $h := g^{-1}$ and substituting.
=== Necessary Condition ===
Suppose that $S$ satisfies $(1)$.
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | l = g \circ S
      | r = S \circ g
      | c = $(1)$
}}
{{eqn | ll= \leadsto
      | l = \paren {g \circ S} \circ g^{-1}
      | r = \paren {S \circ g} \circ g^{-1}
}}
{{eqn | ll= \leadsto
      | l = g \circ S \circ g^{-1}
      | r = S \circ \paren {g \circ g^{-1} }
      | c = Subset Product within Semigroup is Associative: Corollary
}}
{{eqn | ll= \leadsto
      | l = g \circ S \circ g^{-1}
      | r = S \circ e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = g \circ S \circ g^{-1}
      | r = S
      | c = Subset Product by Identity Singleton
}}
{{eqn | ll= \leadsto
      | l = g^{-1} \circ S \circ g
      | r = S
      | c = $(4)$
}}
{{end-eqn}}
{{qed|lemma}}
=== Sufficient Condition ===
Suppose that $S$ satisfies $(2)$ or $(3)$.
By $(4)$, as long as one of these statements holds, the other one holds as well.
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | l = g \circ S \circ g^{-1}
      | r = S
}}
{{eqn | ll= \leadsto
      | l = \paren {g \circ S \circ g^{-1} } \circ g
      | r = S \circ g
}}
{{eqn | ll= \leadsto
      | l = \paren {g \circ S} \circ \paren {g^{-1} \circ g}
      | r = S \circ g
      | c = Subset Product within Semigroup is Associative: Corollary
}}
{{eqn | ll= \leadsto
      | l = \paren {g \circ S} \circ e
      | r = S \circ g
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = g \circ S
      | r = S \circ g
      | c = Subset Product by Identity Singleton
}}
{{end-eqn}}
{{qed}}