avewright/proofwiki-math huggingface dataset:
Theorem: Floquet's Theorem

Let $\mathbf A \left({t}\right)$ be a continuous matrix function with period $T$.
Let $\Phi \left({t}\right)$ be a fundamental matrix of the Floquet system $\mathbf x' = \mathbf A \left({t}\right) \mathbf x$.
Then $\Phi \left({t + T}\right)$ is also a fundamental matrix.
Moreover, there exists:
: A nonsingular, continuously differentiable matrix function $\mathbf P \left({t}\right)$ with period $T$
: A constant (possibly complex) matrix $\mathbf B$ such that:
::$\Phi \left({t}\right) = \mathbf P \left({t}\right) e^{\mathbf Bt}$

Proof:
Let $\map S t = \map \Phi {t + T} {\map \Phi T}^{-1}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d t} } {\map S t}
      | r = \map {\Phi'} {t + T} {\map \Phi T}^{-1}
      | c = 
}}
{{eqn | r = \map {\mathbf A} {t + T} \map \Phi {t + T} {\map \Phi T}^{-1}
      | c = 
}}
{{eqn | r = \map {\mathbf A} t \map S t
      | c = 
}}
{{end-eqn}}
So $\map S t$ is a fundamental matrix and:
:$\map S 0 = Id$
Then:
:$\map S t = \map \Phi t$
which means that:
:$\map \Phi {t + T} = \map \Phi t \map \Phi T$
Hence by the existence of the matrix logarithm, there exists a matrix $\mathbf B$ such that:
:$\map \Phi T = e^{\mathbf B T}$
Defining $\map {\mathbf P} t = \map \Phi t e^{-\mathbf B t}$, it follows that:
{{begin-eqn}}
{{eqn | l = \map {\mathbf P} {t + T}
      | r = \map \Phi {t + T} e^{-\mathbf B t - \mathbf B T}
      | c = 
}}
{{eqn | r = \map \Phi t \map \Phi T e^{-\mathbf B T} e^{-\mathbf B t}
      | c = 
}}
{{eqn | r = \map \Phi t e^{-\mathbf B t}
      | c = 
}}
{{eqn | r = \map {\mathbf P} t
      | c = 
}}
{{end-eqn}}
and hence $\map {\mathbf P} t$ is a periodic real function with period $T$.
As $\map \Phi t = \map {\mathbf P} t e^{\mathbf B t}$, the second implication also holds.
{{qed}}
Theorem: Lyapunov's Stability Theorem

Let $V$ be a Lyapunov function on an open set containing an equilibrium point $x_0$.
{{Disambiguate|Definition:Open Set}}
Then $x_0$ is stable.
If $V$ is strict, then $x_0$ is asymptotically stable.
{{explain|strict}}

Proof:
{{ProofWanted}}
{{Namedfor|Aleksandr Mikhailovich Lyapunov|cat = Lyapunov}}
Category:Differential Equations
Category:Lyapunov Functions
mpigav5ix0mmnldur1vtkr6u6msegch
Theorem: Bendixson-Dulac Theorem

Suppose there exists a continuously differentiable function $\map \alpha {x, y}$ on a simply connected domain.
{{Explain|What ''is'' the domain? Reals, complex, or what?}}
Suppose that:
:$\nabla \cdot \paren {\alpha F}$
is either always positive or always negative.
Then the two-dimensional autonomous system:
:$\tuple {x, y}' = \map F {x, y}$
does not have a periodic solution.

Proof:
{{ProofWanted}}
{{Namedfor|Ivar Otto Bendixson|name2 = Henri Claudius Rosaris Dulac|cat = Bendixson|cat2 = Dulac}}
Category:Differential Equations
ic5qrm85zv86t44pyutgh5gq7c0o48o
Theorem: General Vector Solution of Fundamental Matrix

Let $\map \Phi t$ be a fundamental matrix of the system $x' = \map A t x$.
Then:
:$\map \Phi t c$ is a general solution of $x' = \map A t x$.

Proof:
By definition, $\map \Phi t$ is non-singular, and therefore has an inverse $\map {\Phi^{-1} } t$.
If $z$ is an arbitrary solution, then $\map \Phi t \, \map {\Phi^{-1} } {t_0} \, \map z {t_0}$ also solves the system and has the same initial condition.
Hence by Existence and Uniqueness Theorem for 1st Order IVPs $\map \Phi t \, \map {\Phi^{-1} } {t_0} \, \map z {t_0}$ equals $z$.
Letting $c = \map {\Phi^{-1} } {t_0} \, \map z {t_0}$ finishes the proof.
{{Qed}}
Category:Differential Equations
renr98uvtijivbi4ynkcskmz82vwl6y
Theorem: General Fundamental Matrix

Let $\map \Phi t$ be a fundamental matrix of the system $x' = \map A t x$.
Then:
:$\map \Phi t C$
is a general fundamental matrix of $x' = \map A t x$, where $C$ is ''any'' nonsingular matrix.

Proof:
$\map \Phi t C$ is a fundamental matrix as follows:
:$\dfrac \d {\d t} \map \Phi t C = \map {\Phi'} t C = \map A t \map \Phi t C$
:$\map \det {\map \Phi t C} = \map \det {\map \Phi t} \map \det C \ne 0$
Let $\map \Psi t$ be an arbitrary fundamental matrix.
Then from General Vector Solution of Fundamental Matrix $\map \Phi t \map {\Phi^{-1} } {t_0} \map \Psi {t_0}$ solves the same matrix equation and has the same initial conditions.
Hence by uniqueness:
:$\map \Phi t \, \map {\Phi^{-1} } {t_0} \map \Psi {t_0}$ is equal to $\map \Psi t$
Letting $C = \map {\Phi^{-1} } {t_0} \map \Psi {t_0}$ finishes the proof.
{{qed}}
Category:Differential Equations
jzg5qiexzf5ra9qbyzwpedbcs92lnko
Theorem: Condition for Composite Mapping on Left

Let $A, B, C$ be sets.
Suppose that $C$ is non-empty.
Let $f: A \to B$ and $g: A \to C$ be mappings.
Let $\RR: B \to C$ be a relation such that $g = \RR \circ f$ is the composite of $f$ and $\RR$.
Then $\RR$ may be a mapping {{iff}}:
:$\forall x, y \in A: \map f x = \map f y \implies \map g x = \map g y$
That is:
:$\forall x, y \in A: \map f x = \map f y \implies \map g x = \map g y$
{{iff}}:
:$\exists h: B \to C$ such that $h$ is a mapping and $h \circ f = g$

Proof:
=== Sufficient Condition ===
Suppose $\forall x, y \in A: \map f x = \map f y \implies \map g x = \map g y$.
Consider the subset $G \subseteq \Img f \times C$ defined by:
:$G = \set {\tuple {y, z}: \exists x \in A: y = \map f x, z =\map g x}$
Clearly $G \ne \O$ because for any $x \in A$ we have $\tuple {\map f x, \map g x} \in G$.
What we need to show is that $G$ is the graph of a mapping $t: \Img f \to C$.
To do that, we need to show that for every $y \in \Img f$, there is a unique $z \in C$ such that $\tuple {y, z} \in G$.
It is clear that there is at least one such $z$: choose any $x \in A$ such that $y = \map f x$ and set $z = \map g x$.
Now we need to show that such a $z$ is unique.
Suppose we have $\tuple {y, z} \in G$ and $\tuple {y, z'} \in G$.
Then by the definition of $G$:
:$\exists x, x' \in A: y = \map f x = \map f {x'}, z = \map g x, z' = \map g {x'}$
We have taken as a hypothesis that:
:$\forall x, y \in A: \map f x = \map f y \implies \map g x = \map g y$
So $\map g x = \map g {x'}$ and so $z = z'$.
So $G$ is the graph of a mapping which we can denote:
:$t: \Img f \to C$
Also, since:
:$\forall x \in A: \tuple {\map f x, \map g x} \in G$
it follows that:
:$\forall x \in A: \map f x = \map t {\map f x}$
Since $C$ is non-empty, it has an element $c$.
By Law of Excluded Middle, we can now construct a mapping $h$ as follows:
:<nowiki>$\map h x = \begin{cases}
   \map t x  & : x \in \Img f \\
   c         & : x \in B \setminus \Img f
\end{cases}$</nowiki>
So:
:$\forall x \in A: \map {\paren {h \circ f} } x = \map h {\map f x} = \map t {\map f x} = \map g x$
Thus we have constructed a mapping $h$ such that $h \circ f = g$, as required.
{{qed|lemma}}
Theorem: Condition for Composite Mapping on Right

Let $A, B, C$ be sets.
Let $f: B \to A$ and $g: C \to A$ be mappings.
Let $\RR: C \to B$ be a relation such that $g = f \circ \RR$ is the composite of $\RR$ and $f$.
Then $\RR$ may be a mapping {{iff}}:
:$\Img g \subseteq \Img f$
That is:
:$\Img g \subseteq \Img f$
{{iff}}:
:$\exists h: C \to B$ such that $h$ is a mapping and $f \circ h = g$

Proof:
=== Sufficient Condition ===
Suppose $\Img g \subseteq \Img f$.
That is:
:$\forall x \in C: \map g x \in \Img f$
and so:
:$\forall x \in C: \exists y \in B: \map g x = \map f y$
Take any $x \in C$.
Consider the set $Y_x = \set {y \in B: \map g x = \map f y}$.
We know from above that $Y_x \ne \O$.
So, using the Axiom of Choice, for each $x$ we may select some $y_x \in Y_x$.
Then we may define the mapping $h: C \to B$ such that:
:$\forall x \in C: \map h x = y_x$
We then see that:
{{begin-eqn}}
{{eqn | q = \forall x \in C
      | l = \map {\paren {f \circ h} } x
      | r = \map f {\map h x}
      | c = 
}}
{{eqn | r = \map f {y_x}
      | c = 
}}
{{eqn | r = \map g x
      | c = 
}}
{{end-eqn}}
Thus we have constructed a mapping $h$ such that $f \circ h = g$, as required.
Theorem: Set Union Preserves Subsets

Let $A, B, S, T$ be sets.
Then:
:$A \subseteq B, \ S \subseteq T \implies A \cup S \subseteq B \cup T$

Proof:
Let $A \subseteq B$, and let $S$ be any set.
From Set Union Preserves Subsets, substituting $S$ for $T$:
:$A \subseteq B, \ S \subseteq S \implies A \cup S \subseteq B \cup S$
From Set is Subset of Itself, $S \subseteq S$ for all sets $S$.
Hence the first result:
:$A \subseteq B \implies A \cup S \subseteq B \cup S$
The second result follows from Union is Commutative.
{{qed}}
Theorem: Set Union Preserves Subsets

Let $A, B, S, T$ be sets.
Then:
:$A \subseteq B, \ S \subseteq T \implies A \cup S \subseteq B \cup T$

Proof:
Let $A$, $B$, and $S$ be sets.
Let $A \subseteq B$.
Let $x \in A \cup S$.
By the definition of union:
:$x \in A$ or $x \in S$
Suppose $x \in A$.
Then by the definition of subset:
:$x \in B$
Thus by the definition of union:
:$x \in B \cup S$
Suppose instead that $x \in S$.
Then by the definition of union:
:$x \in B \cup S$
Thus for all $x \in A \cup S$:
:$x \in B \cup S$
The second result follows from Union is Commutative.
{{qed}}
Theorem: Set Union Preserves Subsets

Let $A, B, S, T$ be sets.
Then:
:$A \subseteq B, \ S \subseteq T \implies A \cup S \subseteq B \cup T$

Proof:
Let $A \subseteq B$ and $S \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = x \in A
      | o = \leadsto
      | r = x \in B
      | c = {{Defof|Subset}}
}}
{{eqn | l = x \in S
      | o = \leadsto
      | r = x \in T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Now we invoke the Constructive Dilemma of propositional logic:
:$p \implies q, \ r \implies s \vdash p \lor r \implies q \lor s$
applying it as:
:$\paren {x \in A \implies x \in B, \ x \in S \implies x \in T} \implies \paren {x \in A \lor x \in S \implies x \in B \lor x \in T}$
The result follows directly from the definition of set union:
:$\paren {x \in A \implies x \in B, \ x \in S \implies x \in T} \implies \paren {x \in A \cup S \implies x \in B \cup T}$
and from the definition of subset:
:$A \subseteq B, \ S \subseteq T \implies A \cup S \subseteq B \cup T$
{{qed}}
Theorem: Set Union Preserves Subsets

Let $A, B, S, T$ be sets.
Then:
:$A \subseteq B, \ S \subseteq T \implies A \cup S \subseteq B \cup T$

Proof:
By Subset Relation is Transitive, $\subseteq$ is a transitive relation.
By the corollary to Set Union Preserves Subsets (Proof 2), $\subseteq$ is compatible with $\cup$.
Thus the theorem holds by Operating on Transitive Relationships Compatible with Operation.
{{qed}}
Theorem: Set Complement inverts Subsets

:$S \subseteq T \iff \map \complement T \subseteq \map \complement S$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap T
      | r = S
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement {S \cap T}
      | r = \map \complement S
      | c = Complement of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement S \cup \map \complement T
      | r = \map \complement S
      | c = De Morgan's Laws: Complement of Intersection
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement T
      | o = \subseteq
      | r = \map \complement S
      | c = Union with Superset is Superset
}}
{{end-eqn}}
{{qed}}
Theorem: Set Complement inverts Subsets

:$S \subseteq T \iff \map \complement T \subseteq \map \complement S$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = (x \in S 
      | o = \implies
      | r = x \in T)
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadstoandfrom
      | l = (x \notin T
      | o = \implies
      | r = x \notin S)
      | c = Rule of Transposition
}}
{{eqn | ll= \leadstoandfrom
      | l = (x \in \map \complement T
      | o = \implies
      | r = x \in \map \complement S)
      | c = {{Defof|Set Complement}}
}}
{{eqn | l = \map \complement T
      | o = \subseteq
      | r = \map \complement S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Complement inverts Subsets

:$S \subseteq T \iff \map \complement T \subseteq \map \complement S$

Proof:
By definition of set complement:
:$\map \complement T := \relcomp {\mathbb U} T$
where:
:$\mathbb U$ is the universal set
:$\relcomp {\mathbb U} T$ denotes the complement of $T$ relative to $\mathbb U$.
Thus the statement can be expressed as:
:$S \subseteq T \iff \relcomp {\mathbb U} T \subseteq \relcomp {\mathbb U} S$
The result then follows from Relative Complement inverts Subsets.
{{qed}}
Theorem: Set Difference with Superset is Empty Set

:$S \subseteq T \iff S \setminus T = \O$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = S \setminus T = \O
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {\exists x: x \in S \land x \notin T}
      | c = {{Defof|Empty Set}}
}}
{{eqn | o = \leadstoandfrom
      | r = \forall x: \neg \paren {x \in S \land x \notin T}
      | c = De Morgan's Laws (Predicate Logic)
}}
{{eqn | o = \leadstoandfrom
      | r = \forall x: x \notin S \lor x \in T
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = \forall x: x \in S \implies x \in T
      | c = Rule of Material Implication
}}
{{eqn | o = \leadstoandfrom
      | r = S \subseteq T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection with Subset is Subset

:$S \subseteq T \iff S \cap T = S$

Proof:
Let $S \cap T = S$.
Then by the definition of set equality, $S \subseteq S \cap T$.
Thus:
{{begin-eqn}}     
{{eqn | l = S \cap T
      | o = \subseteq
      | r = T
      | c = Intersection is Subset
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = T
      | c = Subset Relation is Transitive
}}
{{end-eqn}}
Now let $S \subseteq T$.
From Intersection is Subset we have $S \supseteq S \cap T$.
We also have:
{{begin-eqn}}     
{{eqn | l = S
      | o = \subseteq
      | r = T
      | c = 
}}
{{eqn | ll= \leadsto
      | l = S \cap S
      | o = \subseteq
      | r = T \cap S
      | c = Set Intersection Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = S \cap T
      | c = Set Intersection is Idempotent and Intersection is Commutative
}}
{{end-eqn}}
So as we have:
{{begin-eqn}}     
{{eqn | l = S \cap T
      | o = \subseteq
      | r = S
}}
{{eqn | l = S \cap T
      | o = \supseteq
      | r = S
}}
{{end-eqn}}
it follows from the definition of set equality that:
:$S \cap T = S$
So we have:
{{begin-eqn}}     
{{eqn | l = S \cap T = S
      | o = \implies
      | r = S \subseteq T
}}
{{eqn | l = S \subseteq T
      | o = \implies
      | r = S \cap T = S
}}
{{end-eqn}}
and so:
:$S \subseteq T \iff S \cap T = S$
from the definition of equivalence.
{{Qed}}
Theorem: Intersection with Subset is Subset

:$S \subseteq T \iff S \cap T = S$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = S \cap T = S
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in S \land x \in T \iff x \in S}
      | c = {{Defof|Set Equality}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in S  \implies x \in T}
      | c = Conditional iff Biconditional of Antecedent with Conjunction
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = S \subseteq T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Union with Superset is Superset

:$S \subseteq T \iff S \cup T = T$

Proof:
Let $S \cup T = T$.
Then by definition of set equality:
:$S \cup T \subseteq T$
Thus:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = S \cup T
      | c = Subset of Union
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = T
      | c = Subset Relation is Transitive
}}
{{end-eqn}}
Now let $S \subseteq T$.
From Subset of Union, we have $S \cup T \supseteq T$.
We also have:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
      | c =
}}
{{eqn | ll= \leadsto
      | l = S \cup T
      | o = \subseteq
      | r = T \cup T
      | c = Set Union Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = S \cup T
      | o = \subseteq
      | r = T
      | c = Set Union is Idempotent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = S \cup T
      | o = \subseteq
      | r = T
      | c = 
}}
{{eqn | l = S \cup T
      | o = \supseteq
      | r = T
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$S \cup T = T$
So:
{{begin-eqn}}
{{eqn | l = S \cup T = T
      | o = \implies
      | r = S \subseteq T
      | c = 
}}
{{eqn | l = S \subseteq T
      | o = \implies
      | r = S \cup T = T
      | c = 
}}
{{end-eqn}}
and so:
:$S \subseteq T \iff S \cup T = T$
from the definition of equivalence.
{{Qed}}
Theorem: Union with Superset is Superset

:$S \subseteq T \iff S \cup T = T$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = S \cup T = T
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in S \lor x \in T \iff x \in T}
      | c = {{Defof|Set Equality}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in S \implies x \in T}
      | c = Conditional iff Biconditional of Consequent with Disjunction
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = S \subseteq T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Intersection with Complement is Empty iff Subset

:$S \subseteq T \iff S \cap \map \complement T = \O$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = S \setminus T
      | r = \O
      | c = Set Difference with Superset is Empty Set
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap \map \complement T
      | r = \O
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Complement Union with Superset is Universe

:$S \subseteq T \iff \map \complement S \cup T = \mathbb U$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap \map \complement T
      | r = \O
      | c = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement {S \cap \map \complement T}
      | r = \mathbb U
      | c = Complement of Empty Set is Universal Set
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement S \cup \map \complement {\map \complement T}
      | r = \mathbb U
      | c = De Morgan's Laws: Complement of Intersection
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement S \cup T
      | r = \mathbb U
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is not Associative

Let $R, S, T$ be sets.
The expression:
:$\paren {R \setminus S} \setminus T = R \setminus \paren {S \setminus T}$
holds exactly when $R \cap T = \O$.
Here $R \setminus S$ denotes set difference.
Thus, set difference is not associative.

Proof:
We assume a universal set $\mathbb U$ such that $R, S, T \subseteq \mathbb U$.
We have the identity Set Difference as Intersection with Complement:
:$R \setminus S = R \cap \overline S$
where $\overline S$ is the set complement of $S$:
:$\overline S = \relcomp {\Bbb U} S$
Thus we can represent the two expressions as follows:
{{begin-eqn}}
{{eqn | l = \paren {R \setminus S} \setminus T
      | r = \paren {R \cap \overline S} \cap \overline T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = R \cap \overline S \cap \overline T
      | c = Intersection is Associative
}}
{{end-eqn}}
For the second:
{{begin-eqn}}
{{eqn | o = 
      | r = R \setminus \paren {S \setminus T}
      | c = 
}}
{{eqn | r = R \cap \overline {\paren {S \cap \overline T} }
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = R \cap \paren {\overline S \cup \overline {\paren {\overline T} } }
      | c = De Morgan's Laws: Complement of Intersection
}}
{{eqn | r = R \cap \paren {\overline S \cup T}
      | c = Complement of Complement
}}
{{eqn | r = \paren {R \cap \overline S} \cup \paren {R \cap T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \cap \overline S \cap \mathbb U} \cup \paren {R \cap \mathbb U \cap T}
      | c = Intersection with Universal Set
}}
{{eqn | r = \paren {R \cap \overline S \cap \paren {T \cup \overline T} } \cup \paren {R \cap \paren {S \cup \overline S} \cap T}
      | c = Union with Complement
}}
{{eqn | r = \paren {R \cap \overline S \cap T} \cup \paren {R \cap \overline S \cap \overline T}
      | c = 
}}
{{eqn | o = 
      | lo= \cup
      | r = \paren {R \cap S \cap T} \cup \paren {R \cap \overline S \cap T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \cap \overline S \cap T} \cup \paren {R \cap \overline S \cap \overline T} \cup \paren {R \cap S \cap T}
      | c = Set Union is Idempotent
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {R \cap \paren {S \cup \overline S} \cap T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {R \cap \mathbb U \cap T}
      | c = Union with Complement
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {R \cap T}
      | c = Intersection with Universal Set
}}
{{end-eqn}}
As can be seen, this full expansion of the second expression can be expressed:
:$R \setminus \paren {S \setminus T} = \paren {\paren {R \setminus S} \setminus T} \cup \paren {R \cap T}$
It directly follows from Intersection with Empty Set that:
:$R \setminus \paren {S \setminus T} = \paren {R \setminus S} \setminus T \iff R \cap T = \O$
{{qed}}
Theorem: Associativity on Four Elements

Let $\struct {S, \circ}$ be a semigroup.
Let $a, b, c, d \in S$.
Then:
:$a \circ b \circ c \circ d$
gives a unique answer no matter how the elements are associated.

Proof:
As $\struct {S, \circ}$ is a semigroup:
: it is closed
: $\circ$ is associative
From Parenthesization of Word of $4$ Elements, there are exactly $5$ different ways of inserting brackets in the expression $a \circ b \circ c \circ d$.
As $\circ$ is associative, we have that:
:$\forall s_1, s_2, s_3 \in S: \paren {s_1 \circ s_2} \circ s_3 = s_1 \circ \paren {s_2 \circ s_3}$
As $\struct {S, \circ}$ is closed, we know that all products of elements from $\set {a, b, c, d}$ are in $S$, and are likewise bound by the associativity of $S$.
So:
{{begin-eqn}}
{{eqn | l = \paren {\paren {a \circ b} \circ c} \circ d
      | r = \paren {a \circ \paren {b \circ c} } \circ d
      | c = 
}}
{{eqn | r = a \circ \paren {\paren {b \circ c} \circ d}
      | c = 
}}
{{eqn | r = a \circ \paren {b \circ \paren {c \circ d} }
      | c = 
}}
{{eqn | r = \paren {a \circ b} \circ \paren {c \circ d}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Group Isomorphism Preserves Identity

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group isomorphism.
Let:
:$e_G$ be the identity of $\struct {G, \circ}$
:$e_H$ be the identity of $\struct {H, *}$.
Then:
:$\map \phi {e_G} = e_H$

Proof:
An group isomorphism is by definition a group epimorphism.
The result follows from Epimorphism Preserves Identity.
{{Qed}}
Theorem: Group Isomorphism Preserves Identity

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group isomorphism.
Let:
:$e_G$ be the identity of $\struct {G, \circ}$
:$e_H$ be the identity of $\struct {H, *}$.
Then:
:$\map \phi {e_G} = e_H$

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {e_G}
      | r = \map \phi {e_G \circ e_G}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \map \phi {e_G} * \map \phi {e_G}
      | c = {{Defof|Group Isomorphism}}
}}
{{eqn | r = \map \phi {e_G} * \map \phi {e_G}
      | c = {{Defof|Group Isomorphism}}
}}
{{end-eqn}}
It follows from Identity is only Idempotent Element in Group that $\map \phi {e_G}$ is the identity of $H$.
That is:
:$\map \phi {e_G} = e_H$
{{qed}}