avewright/proofwiki-math huggingface dataset:
Theorem: Real Number is not necessarily Rational Number

Let $x$ be a real number.
Then it is not necessarily the case that $x$ is also a rational number.

Proof:
By Proof by Counterexample:
Let $x = \sqrt 2$.
From Square Root of 2 is Irrational:
:$\sqrt 2$ is an irrational number.
By definition:
:$x \in \R \setminus \Q$
where:
:$\R$ is the set of real numbers
:$\Q$ is the set of rational numbers
:$\setminus$ denotes the set difference.
Thus $x$, while being a real number, is not also a rational number.
Hence the result.
{{qed}}
Theorem: Zero is both Positive and Negative

The number $0$ (zero) is the only (real) number which is both:
:a positive (real) number
and
:a negative (real) number.

Proof:
Let $x$ be a real number which is both positive and negative.
Thus:
:$x \in \set {x \in \R: x \ge 0}$
and:
:$x \in \set {x \in \R: x \le 0}$
and so:
:$0 \le x \le 0$
from which:
:$x = 0$
{{qed}}
Theorem: Binary Operation on Subset is Binary Operation

Let $S$ be a set.
Let $\circ$ be a binary operation on $S$.
Let $T \subseteq S$.
Let $\circ {\restriction}_T$ be the restriction of $\circ$ to $T$.
Then $\circ {\restriction}_T$ is a binary operation on $T$.

Proof:
Let $\Bbb U$ be a universal set.
Let $\circ: S \times S \to \Bbb U$ be a binary operation on $S$.
Let $T \subseteq S$.
Let $\tuple {a, b} \in T \times T$.
By definition of ordered pair and cartesian product:
:$a \in T$ and $b \in T$
As $T \subseteq S$, it follows that:
:$a \in S$ and $b \in S$
Thus:
:$\tuple {a, b} \in S \times S$
As $\circ$ is a binary operation on $S$, it follows that:
:$\map \circ {a, b} \in \Bbb U$
But by definition of restriction of $\circ$:
:$\map \circ {a, b} = \map {\circ {\restriction}_T} {a, b}$
Thus:
:$\map {\circ {\restriction}_T} {a, b} \in \Bbb U$
As $a$ and $b$ are arbitrary elements of $T$, it follows that this holds for all $a, b \in T$.
Hence the result by definition of binary operation.
{{qed}}
Category:Binary Operations
qkpe5350axo8x4cydaj7pd4l6yy0qv0
Theorem: Matrix Entrywise Addition over Ring is Associative

Let $\struct {R, +, \circ}$ be a ring.
Let $\map {\MM_R} {m, n}$ be a $m \times n$ matrix space over $R$.
For $\mathbf A, \mathbf B \in \map {\MM_R} {m, n}$, let $\mathbf A + \mathbf B$ be defined as the matrix entrywise sum of $\mathbf A$ and $\mathbf B$.
The operation $+$ is associative on $\map {\MM_R} {m, n}$.
That is:
:$\paren {\mathbf A + \mathbf B} + \mathbf C = \mathbf A + \paren {\mathbf B + \mathbf C}$
for all $\mathbf A$, $\mathbf B$ and $\mathbf C$ in $\map {\MM_R} {m, n}$.

Proof:
Let $\mathbf A = \sqbrk a_{m n}$, $\mathbf B = \sqbrk b_{m n}$ and $\mathbf C = \sqbrk c_{m n}$ be elements of the $m \times n$ matrix space over $R$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\mathbf A + \mathbf B} + \mathbf C
      | r = \paren {\sqbrk a_{m n} + \sqbrk b_{m n} } + \sqbrk c_{m n}
      | c = Definition of $\mathbf A$, $\mathbf B$ and $\mathbf C$
}}
{{eqn | r = \sqbrk {a + b}_{m n} + \sqbrk c_{m n}
      | c = {{Defof|Matrix Entrywise Addition over Ring}}
}}
{{eqn | r = \sqbrk {\paren {a + b} + c}_{m n}
      | c = {{Defof|Matrix Entrywise Addition over Ring}}
}}
{{eqn | r = \sqbrk {a + \paren {b + c} }_{m n}
      | c = {{Ring-axiom|A1}}
}}
{{eqn | r = \sqbrk a_{m n} + \sqbrk {b + c}_{m n}
      | c = {{Defof|Matrix Entrywise Addition over Ring}}
}}
{{eqn | r = \sqbrk a_{m n} + \paren {\sqbrk b_{m n} + \sqbrk c_{m n} }
      | c = {{Defof|Matrix Entrywise Addition over Ring}}
}}
{{eqn | r = \mathbf A + \paren {\mathbf B + \mathbf C}
      | c = Definition of $\mathbf A$, $\mathbf B$ and $\mathbf C$
}}
{{end-eqn}}
{{qed}}
Theorem: Matrix Entrywise Addition over Ring is Associative

Let $\struct {R, +, \circ}$ be a ring.
Let $\map {\MM_R} {m, n}$ be a $m \times n$ matrix space over $R$.
For $\mathbf A, \mathbf B \in \map {\MM_R} {m, n}$, let $\mathbf A + \mathbf B$ be defined as the matrix entrywise sum of $\mathbf A$ and $\mathbf B$.
The operation $+$ is associative on $\map {\MM_R} {m, n}$.
That is:
:$\paren {\mathbf A + \mathbf B} + \mathbf C = \mathbf A + \paren {\mathbf B + \mathbf C}$
for all $\mathbf A$, $\mathbf B$ and $\mathbf C$ in $\map {\MM_R} {m, n}$.

Proof:
By definition, matrix entrywise addition is the '''Hadamard product''' of $\mathbf A$ and $\mathbf B$ with respect to ring addition.
We have from {{Ring-axiom|A1}} that ring addition is associative.
The result then follows directly from Associativity of Hadamard Product.
{{qed}}
Theorem: Sum of Möbius Function over Divisors

:$\ds \sum_{d \mathop \divides n} \map \mu d = \floor {\frac 1 n}$
where $\floor {\dfrac 1 n}$ is the floor of $\dfrac 1 n$.

Proof:
The theorem is clearly true if $n = 1$.
Assume, then, that $n > 1$ and write, by the Fundamental Theorem of Arithmetic:
:$n = p_1^{a_1} p_2^{a_2} \dots p_k^{a_k}$
In the sum $\ds \sum_{d \mathop \divides n} \map \mu d$ the only non-zero terms come from $d = 1$ and the divisors of $n$ which are products of distinct primes.
From the definition of the Möbius function, the Möbius function of a product of $m$ distinct primes is $\paren {-1}^m$.
From the definition of Binomial coefficient, there are $\dbinom k m$ ways to choose $m$ primes from $p_1, p_2, \dots, p_k$ to multiply together.
So among the divisors of $p_1 p_2 \dotsm p_k$, there are exactly $\dbinom k m$ numbers that are the product of $m$ distinct primes.
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{d \mathop \divides n} \map \mu d
      | r = \map \mu 1 + \map \mu {p_1} + \dotsb + \map \mu {p_k} + \map \mu {p_1 p_2} + \dotsb + \map \mu {p_{k - 1} p_k} + \dotsb + \map \mu {p_1 p_2 \dotsm p_k}
      | c = 
}}
{{eqn | r = \dbinom k 0 + \dbinom k 1 \paren {-1} + \dbinom k 2 \paren {-1}^2 + \cdots + \dbinom k k \paren {-1}^k
      | c = 
}}
{{eqn | r = 0
      | c = Alternating Sum and Difference of Binomial Coefficients for Given n
}}
{{end-eqn}}
Hence, the sum is $1$ for $n = 1$, and $0$ for $n > 1$, which are precisely the values of $\floor {\dfrac 1 n}$.
{{qed}}
Theorem: Final Topology with respect to Mapping

Let $\struct {X, \tau_X}$ be a topological space.
Let $Y$ be a set.
Let $f: X \to Y$ be a mapping.
Let $\tau_Y$ be the final topology on $Y$ {{WRT}} $f$.
Then:
:$\tau_Y = \set {U \subseteq Y : f^{-1} \sqbrk U \in \tau_X}$
Observe that the set on the {{RHS}} of the equality is sometimes denoted $f\tau$.
Further, the following holds true:
# $\forall \struct {Z, \tau_Z}$ topological space $\forall g: \struct {Y, f \tau} \to \struct {Z, \tau_Z}$ mapping $g$ is continuous $\iff g \circ f$ is continuous (where $f$ is defined from $\struct {X, \tau_X}$ to $\struct {Y, f \tau}$).
# $\forall \tau_Y$ topology in $Y : \forall \struct {Z, \tau_Z}$ topological space, the following are equivalent:
##$\tau_Y = f \tau$
##$\forall g: \struct {Y, \tau_Y} \to \struct {Z, \tau_Z}: g$ is continuous $\iff g \circ f$ is continuous (where $f$ is defined from $\struct {X, \tau_X}$ to $\struct {Y, \tau_Y}$).
That is, the topology $f \tau$ is ''characterised'' by the fact that it is the only one which makes all mappings defined from it to any topological space continuous.

Proof:
{{proof wanted}}
Category:Topology
qthidr0arb1dy6iz4bp08pivrosem5e
Theorem: Composition of Symmetries is Symmetry

Let $P$ be a geometric figure.
Let $S_P$ be the set of all symmetries of $P$.
Let $\circ$ denote composition of mappings.
Let $\phi$ and $\psi$ be symmetries of $P$.
Then $\phi \circ \psi$ is also a symmetry of $P$.

Proof:
By definition of composition of mappings:
:$\phi \circ \psi$ is a mapping.
We have by definition of symmetry that:
:$\map \phi P$ is congruent to $P$
and:
:$\map \psi {\map \phi P}$ is congruent to $\map \phi P$
Therefore:
:$\phi \circ \psi$ is congruent to $P$
Thus $\phi \circ \psi$ is a symmetry of $P$.
{{qed}}
Theorem: Composition of Symmetries is Associative

Let $P$ be a geometric figure.
Let $S_P$ be the set of all symmetries of $P$.
Let $\circ$ denote composition of mappings.
Let $\phi, \psi, \chi$ be symmetries of $P$.
Then:
:$\paren {\phi \circ \psi} \circ \chi = \phi \circ \paren {\psi \circ \chi}$
That is, composition of symmetries is associative.

Proof:
From Composition of Symmetries is Symmetry:
:$\paren {\phi \circ \psi} \circ \chi$ is a symmetry
and:
:$\phi \circ \paren {\psi \circ \chi}$ is a symmetry.
It follows from Composition of Mappings is Associative that:
:$\paren {\phi \circ \psi} \circ \chi = \phi \circ \paren {\psi \circ \chi}$
{{qed}}
Theorem: Square of Modulo less One equals One

Let $m \in \Z$ be an integer.
Let $\Z_m$ be the set of integers modulo $m$:
:$\Z_m = \set {\eqclass 0 m, \eqclass 1 m, \ldots, \eqclass {m - 1} m}$
Then:
:$\eqclass {m - 1} m \times_m \eqclass {m - 1} m = \eqclass 1 m$
where $\times_m$ denotes multiplication modulo $m$.

Proof:
{{begin-eqn}}
{{eqn | l = \eqclass {m - 1} m \times_m \eqclass {m - 1} m
      | r = \eqclass {\paren {m - 1}^2} m
      | c = {{Defof|Modulo Multiplication}}
}}
{{eqn | r = \eqclass {m^2 - 2 m + 1} m
      | c = 
}}
{{eqn | r = \eqclass 1 m
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Existence of Non-Square Residue

Let $m \in \Z$ be an integer such that $m > 2$.
Let $\Z_m$ be the set of integers modulo $m$:
:$\Z_m = \set {\eqclass 0 m, \eqclass 1 m, \ldots, \eqclass {m - 1} m}$
Then there exists at least one residue in $\Z_m$ which is not the product modulo $m$ of a residue with itself:
:$\exists p \in \Z_m: \forall x \in \Z_m: x \cdot_m x \ne p$

Proof:
We have that $1 \in \Z_m$ and that:
:$1 \cdot_m 1 = 1$
We have that $m - 1 \in \Z_m$ and that:
:$\paren {m - 1} \cdot_m \paren {m - 1} = 1$
Thus unless $m - 1 = 1$, that is, $m = 2$, there exist $2$ residues of $\Z_m$ whose product modulo $m$ with itself equals $1$.
There are $m - 2$ residues which, when multiplied modulo $m$ with themselves have as a result a residue.
Thus there can be at maximum $m - 2$ residues (excluding $1$) which can be the product modulo $m$ of a residue with itself.
But there are $m - 1$ residues (excluding $1$).
So at least $1$ residue is not the product modulo $m$ of a residue with itself.
{{qed}}
Theorem: Symmetry Group of Equilateral Triangle is Symmetric Group

Let $D_3$ denote the symmetry group of the equilateral triangle.
Let $S_3$ denote the symmetric group on $3$ letters.
Then $D_3$ is isomorphic to $S_3$.

Proof:
{{proofread}}
Follows from Symmetric Group on 3 Letters is Isomorphic to Dihedral Group D3.
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/General Case/Complement of Intersection

:$\ds \relcomp S {\bigcap \mathbb T} = \bigcup_{H \mathop \in \mathbb T} \relcomp S H$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S {\bigcap \mathbb T}
      | r = S \setminus \paren {\bigcap \mathbb T}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \bigcup_{H \mathop \in \mathbb T} \paren {S \setminus H}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \bigcup_{H \mathop \in \mathbb T} \relcomp S H
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/General Case/Complement of Union

:$\ds \relcomp S {\bigcup \mathbb T} = \bigcap_{H \mathop \in \mathbb T} \relcomp S H$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S {\bigcup \mathbb T}
      | r = S \setminus \paren {\bigcup \mathbb T}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \bigcap_{H \mathop \in \mathbb T} \paren {S \setminus H}
      | c = De Morgan's Laws: Difference with Union
}}
{{eqn | r = \bigcap_{H \mathop \in \mathbb T} \relcomp S H
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/Family of Sets/Complement of Union

:$\ds \relcomp S {\bigcup_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} \relcomp S {S_i}$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S {\bigcup_{i \mathop \in I} S_i}
      | r = S \setminus \paren {\bigcup_{i \mathop \in I} S_i}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \bigcap_{i \mathop \in I} \paren {S \setminus S_i}
      | c = De Morgan's Laws for Set Difference: Difference with Union
}}
{{eqn | r = \bigcap_{i \mathop \in I} \relcomp S {S_i}
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/Family of Sets/Complement of Intersection

:$\ds \relcomp S {\bigcap_{i \mathop \in I} S_i} = \bigcup_{i \mathop \in I} \relcomp S {S_i}$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp S {\bigcap_{i \mathop \in I} S_i}
      | r = S \setminus \paren {\bigcap_{i \mathop \in I} S_i}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \bigcup_{i \mathop \in I} \paren {S \setminus S_i}
      | c = De Morgan's Laws for Set Difference: Difference with Intersection
}}
{{eqn | r = \bigcup_{i \mathop \in I} \relcomp S {S_i}
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/Complement of Union

:$\relcomp S {T_1 \cup T_2} = \relcomp S {T_1} \cap \relcomp S {T_2}$

Proof:
Let $x \in S$ througout.
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1 \cup T_2}
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1 \cup T_2} \subseteq \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1} \cap \relcomp S {T_2} \subseteq \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
By definition of set equality:
:$\relcomp S {T_1 \cup T_2} = \relcomp S {T_1} \cap \relcomp S {T_2}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement/Complement of Intersection

:$\relcomp S {T_1 \cap T_2} = \relcomp S {T_1} \cup \relcomp S {T_2}$

Proof:
Let $T_1, T_2 \subseteq S$.
Then from Intersection is Subset and Subset Relation is Transitive:
:$T_1 \cap T_2 \subseteq S$
Hence:
{{begin-eqn}}
{{eqn | l = \relcomp S {T_1 \cap T_2}
      | r = S \setminus \paren {T_1 \cap T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \relcomp S {T_1} \cup \relcomp S {T_2}
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/Family of Sets/Difference with Intersection

:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
where:
:$\ds \bigcup_{i \mathop \in I} T_i := \set {x: \exists i \in I: x \in T_i}$
that is, the union of $\family {T_i}_{i \mathop \in I}$.

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap_{i \mathop \in I} T_i$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcap_{i \mathop \in I} T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap_{i \mathop \in I} T_i
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall i \in I}
      | l = x
      | o = \in
      | r = \rightparen {T_i}
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = x
      | o = \notin
      | r = T_i
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = x
      | o = \in
      | r = S \setminus T_i
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}
      | c = {{Defof|Union of Family}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/Family of Sets/Difference with Union

:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
where:
:$\ds \bigcap_{i \mathop \in I} T_i := \set {x: \forall i \in I: x \in T_i}$
that is, the intersection of $\family {T_i}_{i \mathop \in I}$.

Proof:
Suppose:
:$\ds x \in S \setminus \bigcup_{i \mathop \in I} T_i$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcup_{i \mathop \in I} T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcup_{i \mathop \in I} T_i
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \nexists i \in I
      | l = x
      | o = \in
      | r = T_i
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \notin
      | r = T_i
      | c = Denial of Existence
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S \setminus T_i
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}
      | c = {{Defof|Intersection of Family}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/General Case/Complement of Intersection

:$\ds \map \complement {\bigcap \mathbb T} = \bigcup_{H \mathop \in \mathbb T} \map \complement H$

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement {\bigcap \mathbb T}
      | r = \mathbb U \setminus \paren {\bigcap \mathbb T}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \bigcup_{H \mathop \in \mathbb T} \paren {\mathbb U \setminus H}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \bigcup_{H \mathop \in \mathbb T} \map \complement H
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/General Case/Complement of Union

:$\ds \map \complement {\bigcup \mathbb T} = \bigcap_{H \mathop \in \mathbb T} \map \complement H$

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement {\bigcup \mathbb T}
      | r = \mathbb U \setminus \paren {\bigcup \mathbb T}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \bigcap_{H \mathop \in \mathbb T} \paren {\mathbb U \setminus H}
      | c = De Morgan's Laws for Set Difference: Difference with Union
}}
{{eqn | r = \bigcap_{H \mathop \in \mathbb T} \map \complement H
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection

:$\overline {T_1 \cap T_2} = \overline T_1 \cup \overline T_2$

Proof:
{{begin-eqn}}
{{eqn | l = \overline {T_1 \cap T_2}
      | r = \mathbb U \setminus \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \paren {\mathbb U \setminus T_1} \cup \paren {\mathbb U \setminus T_2}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \overline {T_1} \cup \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection

:$\overline {T_1 \cap T_2} = \overline T_1 \cup \overline T_2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cap T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \land x \in T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \lor \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Disjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \lor x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cup \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cap T_2} = \overline {T_1} \cup \overline {T_2}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection

:$\overline {T_1 \cap T_2} = \overline T_1 \cup \overline T_2$

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement {\map \complement A \cup \map \complement B}
      | r = \map \complement {\map \complement A} \cap \map \complement {\map \complement B}
      | c = De Morgan's Laws: Complement of Union
}}
{{eqn | r = A \cap B
      | c = Complement of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement {\map \complement {\map \complement A \cup \map \complement B} }
      | r = \map \complement {A \cap B}
      | c = taking complements of both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement A \cup \map \complement B
      | r = \map \complement {A \cap B}
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Complement/Complement of Union

:$\overline {T_1 \cup T_2} = \overline T_1 \cap \overline T_2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cup T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \land \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Conjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \land x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cap \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cup T_2} = \overline {T_1} \cap \overline {T_2}$
{{qed}}