avewright/proofwiki-math huggingface dataset:
Theorem: No Membership Loops

For any proper classes or sets $A_1, A_2, \ldots, A_n$:
:$\neg \paren {A_1 \in A_2 \land A_2 \in A_3 \land \cdots \land A_n \in A_1}$

Proof:
{{NotZFC}}
Either $A_1, A_2, \ldots, A_n$ are all sets, or there exists a proper class $A_m$ such that $1 \le m \le n$.
Suppose there exists a proper class $A_m$.
Then, by the definition of a proper class, $\neg A_m \in A_{m+1}$, since it is not a member of any class.
The result then follows directly.
Otherwise it follows that all $A_1, A_2, \ldots, A_n$ are sets.
Then, by the fact that Epsilon Relation is Strictly Well-Founded and a Strictly Well-Founded Relation has no Relational Loops, it follows that: 
:$\neg \paren {A_1 \in A_2 \land A_2 \in A_3 \land \cdots \land A_n \in A_1}$
{{qed}}
Theorem: Composite of Isomorphisms is Isomorphism/Algebraic Structure

Let:
:$\struct {S_1, \odot_1, \odot_2, \ldots, \odot_n}$
:$\struct {S_2, *_1, *_2, \ldots, *_n}$
:$\struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be algebraic structures.
Let:
:$\phi: \struct {S_1, \odot_1, \odot_2, \ldots, \odot_n} \to \struct {S_2, *_1, *_2, \ldots, *_n}$
:$\psi: \struct {S_2, *_1, *_2, \ldots, *_n} \to \struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be isomorphisms.
Then the composite of $\phi$ and $\psi$ is also an isomorphism.

Proof:
If $\phi$ and $\psi$ are both isomorphisms, then they are by definition:
:homomorphisms
:bijections.
From Composite of Homomorphisms on Algebraic Structure is Homomorphism:
:$\phi \circ \psi$ and $\psi \circ \phi$ are both homomorphisms.
From Composite of Bijections is Bijection:
:$\phi \circ \psi$ and $\psi \circ \phi$ are both bijections.
Hence by definition both are also isomorphisms.
{{qed}}
Theorem: Composite of Isomorphisms is Isomorphism/R-Algebraic Structure

Let:
:$\struct {S_1, \ast_1}_R$
:$\struct {S_2, \ast_2}_R$
:$\struct {S_3, \ast_3}_R$
be $R$-algebraic structures with the same number of operations.
Let:
:$\phi: \struct {S_1, \ast_1}_R \to \struct {S_2, \ast_2}_R$
:$\psi: \struct {S_2, \ast_2}_R \to \struct {S_3, \ast_3}_R$
be isomorphisms.
Then the composite of $\phi$ and $\psi$ is also an isomorphism.

Proof:
If $\phi$ and $\psi$ are both isomorphisms, then they are by definition:
:homomorphisms
;bijections.
So:
:From Composite of Homomorphisms for R-Algebraic Structures is Homomorphism we have that $\phi \circ \psi$ and $\psi \circ \phi$ are both homomorphisms
:From Composite of Bijections is Bijection we have that $\phi \circ \psi$ and $\psi \circ \phi$ are both bijections;
and hence by definition also isomorphisms.
{{qed}}
Category:Composite of Isomorphisms is Isomorphism
Category:Isomorphisms (Abstract Algebra)
emgsjpfxnx7h4gcm4ev059htristsz6
Theorem: Element of Transitive Class

Let $B$ be a transitive class.
Then:
:$A \in B \implies A \subsetneq B$
where $\subsetneq$ denotes a proper subset).

Proof:
{{NotZFC}}
By the definition of a transitive class:
:$A \in B \implies A \subseteq B$
But $A \ne B$ because $\paren {A = B \land A \in B} \implies A \in A$, which by No Membership Loops is a contradiction.
Therefore $A \subsetneq B$.
{{qed}}
Theorem: Tangent Line to Convex Graph

Let $f$ be a real function that is:
:continuous on some closed interval $\closedint a b$
:differentiable and convex on the open interval $\openint a b$. 
Then all the tangent lines to $f$ are below the graph of $f$.
{{explain|"below"}}

Proof:
:500px
Let $\TT$ be the tangent line to $f$ at some point $\tuple {c, \map f c}$, $c \in \openint a b$.
Let the gradient of $\TT$ be $m$.
Let $\tuple {x_1, y_1}$ be an arbitrary point on $\TT$.
From the point-slope form of a straight line:
{{begin-eqn}}
{{eqn | l = y - y_1
      | r = m \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = m \paren {x - x_1} + y_1
      | c = 
}}
{{end-eqn}}
For $\TT$:
:$y = \map \TT x$
:$y_1 = \map f c$
:$m = \map {f'} c$
:$x = x$
:$x_1 = c$
so:
:$\map \TT x = \map {f'} c \paren {x - c} + \map f c$
Consider the graph of $f$ to the right of $\tuple {c, \map f c}$, that is, any $x$ in $\openint c b$. 
Let $d$ be the directed vertical distance from  $\TT$ to the graph of $f$.
That is, if $f$ is above $\TT$ then $d > 0$.
If $f$ is below $\TT$, then $d < 0$. 
(From the diagram, it is apparent that $\TT$ is below $f$, but we shall prove it analytically.)
$d$ can be evaluated by:
{{begin-eqn}}
{{eqn | l = d
      | r = \map f x - \map \TT x
      | c = 
}}
{{eqn | r = \map f x - \map {f'} c \paren {x - c} - \map f c
      | c = 
}}
{{eqn | r = \map f x - \map f c - \map {f'} c \paren {x - c}
      | c = 
}}
{{end-eqn}}
By the Mean Value Theorem, there exists some constant $k$ in $\openint c b$ such that:
{{begin-eqn}}
{{eqn | l = \map {f'} k
      | r = \frac {\map f x - \map f c} {x - c}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f'} k \paren {x - c}
      | r = \map f x - \map f c
      | c = 
}}
{{end-eqn}}
Substitute this into the formula for $d$:
{{begin-eqn}}
{{eqn | l = d
      | r = \map {f'} k \paren {x - c} - \map {f'} c \paren {x - c}
      | c = 
}}
{{eqn | r = \paren {\map {f'} k - \map {f'} c} \paren {x - c}
      | c = 
}}
{{end-eqn}}
Recall that $x$ lies in the interval $\openint c b$.
So $x > c$, and the quantity $x - c$ is (strictly) positive.
$k$ is also in the interval $\openint c b$ and so $k > c$.
By construction, $f$ is convex. 
By the definition of convex:
:$k > c \implies \map {f'} k > \map {f'} c$
which means that:
:$\paren {\map {f'} k - \map {f'} c} > 0$
Then $d$ is the product of two (strictly) positive quantities and is itself (strictly) positive. 
Similarly, consider the graph of $f$ to the left of $\tuple {c, \map f c}$, that is, any $x$ in $\openint a c$.
By the same process as above, we will have:
:$d = \paren {\map {f'} k - \map {f'} c} \paren {x - c}$
This time, $x < c$ and the quantity $x - c$ is (strictly) negative.
Further, $k < c$, and so by a similar argument as above:
:$k < c \implies \map {f'} k < \map {f'} c$
and the quantity $\paren {\map {f'} k - \map {f'} c}$ is also (strictly) negative.
Thus $d$ will be the product of two (strictly) negative quantities, and will again be (strictly) positive. 
{{qed}}
Theorem: Characterization of Lower Semicontinuity

Let $f: S \to \overline \R$ be an extended real valued function.
Let $S$ be endowed with a topology $\tau$.
The following are equivalent:
:$(1): \quad$ $f$ is lower semicontinuous (LSC) on $S$.
:$(2): \quad$ All lower level sets of $f$ are closed in $S$.
:$(3): \quad$ The epigraph $\map {\operatorname{epi}} f$ of $f$ is a closed set in $S \times \R$ with the product topology.

Proof:
For each $x_0 \in S$, let $\map \mho {x_0}$ be the set of open neighborhoods of $x_0$ in $\struct {X, \tau}$.
Theorem: Restriction of Strictly Well-Founded Relation is Strictly Well-Founded

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR \subseteq S \times S$ be a strictly well-founded relation on $S$.
Let $T \subseteq S$ be a subset of $S$.
Let $\RR {\restriction_T} \subseteq T \times T$ be the restriction of $\RR$ to $T$.
Then $\RR {\restriction_T}$ is a strictly well-founded relation on $T$.

Proof:
By definition of strictly well-founded relation, every non-empty subset of $S$ has a minimal element.
By Subset Relation is Transitive, every subset of $T$ is also a subset of $S$.
Therefore every non-empty subset of $T$ has a minimal element.
Thus by definition, $\RR$ is a strictly well-founded relation on $T$.
{{qed}}
Theorem: Restriction of Strict Well-Ordering is Strict Well-Ordering

Let $R$ be a strict well-ordering of $A$.
Let $B \subseteq A$.
Then $R$ is a strict well-ordering of $B$.

Proof:
By Restriction of Strictly Well-Founded Relation is Strictly Well-Founded, $R$ is a strictly well-founded relation on $B$.
By Restriction of Total Ordering is Total Ordering, $R$ is a total ordering on $B$.
By the above two statements, $R$ is a strict well-ordering of $B$.
{{explain|Indicate the specific definition which identifies that a foundation relation which is a total ordering is a well-ordering.}}
{{qed}}
Theorem: Alternative Definition of Ordinal

A set $S$ is an ordinal {{iff}} $S$ is transitive and is strictly well-ordered by the $\in$-relation.

Proof:
=== Necessary Condition ===
Suppose that $S$ is an ordinal.
Then $S$ is transitive.
By definition, the strict well-ordering on $S$ is given by the $\in$-relation.
Hence, the necessary condition is satisfied.
{{qed|lemma}}
Theorem: Class of All Ordinals is Ordinal

The class of all ordinals $\On$ is an ordinal.
{{explain|Does this not contradict Class of All Ordinals is Proper Class? Sorry, I now read the discussion page. But the current Definition:Ordinal requires an ordinal to be a set, so $\On$ isn't an ordinal. We need a scond definition of ordinal for this theorem.}}

Proof:
{{questionable|This whole proof probably needs to be rewritten from scratch.}}
{{NotZFC}}
The epsilon relation is equivalent to the strict subset relation when restricted to ordinals by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
It follows that:
:$\forall x \in \On: x \subset \On$
{{explain|We have a problem here since $\On$ is a proper class. The notation $\in $ an $\subseteq$ can naturally be extended to classes, but one must be careful with their use.}}
The initial segment of the class of all ordinals is:
:$\set {x \in \On : x \subset \On}$
{{explain|What is meant by $\subset$ here: $\subseteq$ or $\subsetneqq$? 
Initial segment makes no sense here because $\On$ is not a set.
<br/>Sorry, but "makes no sense" is a bit strong: "initial segment" has been defined on {{ProofWiki}} in the context of a well-ordered set, but the term makes perfect sense if defined in the context of a class.}}
This class is equal to $\On$.
Therefore, by the definition of ordinal, $\On$ is an ordinal.
{{qed}}
Theorem: Transitive Set is Proper Subset of Ordinal iff Element of Ordinal

Let $A$ be an ordinal.
Let $B$ be a transitive set.
Then:
:$B \subsetneq A \iff B \in A$

Proof:
=== Necessary Condition ===
Suppose that $B \in A$.
From Ordinal is Transitive, it follows that $B \subseteq A$.
Also, $B \ne A$ by Ordinal is not Element of Itself.
Therefore, $B \subsetneq A$, as desired.
{{qed|lemma}}
Theorem: Integral of Arcsine Function

:$\ds \int \arcsin x \rd x = x \arcsin x + \sqrt {1 - x^2} + C$
for $x \in \closedint {-1} 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \arcsin x \rd x
      | r = \int 1 \cdot \arcsin x \rd x
}}
{{eqn | r = x \arcsin x - \int x \paren {\frac \rd {\rd x} \arcsin x} \rd x
      | c = Integration by Parts
}}
{{eqn | r = x \arcsin x - \int \frac x {\sqrt {1 - x^2} } \rd x
      | c = Derivative of Arcsine Function
}}
{{end-eqn}}
Substitute:
{{begin-eqn}}
{{eqn | l = u 
      | r = 1 - x^2
}}
{{eqn | l = \frac {\d u} {\d x}
      | r = -2 x
      | c = differentiating {{WRT|Differentiation}} $x$
}}
{{eqn | ll = \leadsto
      | l = -\frac 1 2 \frac {\d u} {\d x}
      | r = x
}}
{{eqn | l = \int \arcsin x \rd x 
      | r = x \arcsin x - \int \frac {- \frac 1 2} {\sqrt u} \frac {\d u} {\d x} \rd x
      | c = Integration by Substitution
}}
{{eqn | r = x \arcsin x + \frac 1 2 \int u^{-1/2} \rd u
      | c = 
}}
{{eqn | r = x \arcsin x + u^{1/2} + C
      | c = Integral of Power
}}
{{eqn | r = x \arcsin x + \sqrt {1 - x^2} + C
      | c = from $u = 1 - x^2$
}}
{{end-eqn}}
{{qed}}
Theorem: Second Derivative of Convex Real Function is Non-Negative

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$.
Then $f$ is convex on $\openint a b$ {{iff}} its second derivative $f' ' \ge 0$ on $\openint a b$.

Proof:
From Real Function is Convex iff Derivative is Increasing, $f$ is convex {{iff}} $f'$ is increasing.
From Derivative of Monotone Function, $f'$ is increasing {{iff}} its second derivative $f' ' \ge 0$.
{{qed}}
Theorem: Ordinal Membership is Trichotomy

Let $\alpha$ and $\beta$ be ordinals.
Then:
:$\paren {\alpha = \beta} \lor \paren {\alpha \in \beta} \lor \paren {\beta \in \alpha}$
where $\lor$ denotes logical or.

Proof:
From Class of All Ordinals is Well-Ordered by Subset Relation, $\On$ is a nest.
Hence:
:$\forall \alpha, \beta \in \On: \paren {\alpha \subsetneqq \beta} \lor \paren {\beta \subsetneqq \alpha} \lor \paren {\alpha = \beta}$
From Transitive Set is Proper Subset of Ordinal iff Element of Ordinal, this is equivalent to:
:$\forall \alpha, \beta \in \On: \paren {\alpha \in \beta} \lor \paren {\beta \in \alpha} \lor \paren {\alpha = \beta}$
Hence the result.
{{qed}}
Theorem: Ordinal Membership is Trichotomy

Let $\alpha$ and $\beta$ be ordinals.
Then:
:$\paren {\alpha = \beta} \lor \paren {\alpha \in \beta} \lor \paren {\beta \in \alpha}$
where $\lor$ denotes logical or.

Proof:
By Relation between Two Ordinals, it follows that:
:$\paren {\alpha = \beta} \lor \paren {\alpha \subset \beta} \lor \paren {\beta \subset \alpha}$
By Transitive Set is Proper Subset of Ordinal iff Element of Ordinal, the result follows.
{{qed}}
Theorem: Second Derivative of Concave Real Function is Non-Positive

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$.
Then $f$ is concave on $\openint a b$ {{iff}} its second derivative $f'' \le 0$ on $\openint a b$.

Proof:
From Real Function is Concave iff Derivative is Decreasing, $f$ is concave {{iff}} $f'$ is decreasing.
From Derivative of Monotone Function, $f'$ is decreasing {{iff}} its second derivative $f'' \le 0$.
{{qed}}
Theorem: Ordinal is Member of Class of All Ordinals

Let $A$ be an ordinal.
Then:
:$A \in \On \lor A = \On$
where $\On$ denotes the class of all ordinals.

Proof:
We have {{hypothesis}} that $A$ is an ordinal
From Class of All Ordinals is Ordinal and Ordinal Membership is Trichotomy:
:$A \in \On \lor A = \On \lor \On \in A$
But by the Burali-Forti Paradox $\On$ is a proper class.
Therefore:
:$A \in \On \lor A = \On$
{{qed}}
{{explain|please say or link to why being a proper class means that $\On \notin A$}}
Theorem: Ordinal is Subset of Class of All Ordinals

Suppose $A$ is an ordinal.
Then:
:$A \subseteq \On$
where $\On$ represents the class of all ordinals.

Proof:
By Ordinal is Member of Class of All Ordinals:
:$A \in \On \lor A = \On$
In either case:
:$A \subseteq \On$
since $\On$ is transitive.
{{explain|Why is $\On$ necessarily transitive? This follows smoothly if it is assumed that $\On$ is a subclass of a Basic Universe, or otherwise from an axiomatic framework. Hence we need to define our axioms here.}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference

{{:De Morgan's Laws (Set Theory)/Set Difference/Difference with Intersection}}

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap \mathbb T$
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 \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall T' \in \mathbb T}
      | l = x
      | o = \in
      | r = \rightparen {T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: Classical Probability is Probability Measure

The classical probability model is a probability measure.

Proof:
We check all the Kolmogorov axioms in turn:
Theorem: De Morgan's Laws (Set Theory)/Set Difference/General Case

Let $S$ and $T$ be sets.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T \subseteq \powerset T$.
Then:
==== Difference with Intersection ====
{{:De Morgan's Laws (Set Theory)/Set Difference/General Case/Difference with Intersection}}
==== Difference with Union ====
{{:De Morgan's Laws (Set Theory)/Set Difference/General Case/Difference with Union}}

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap \mathbb T$
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 \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall T' \in \mathbb T}
      | l = x
      | o = \in
      | r = \rightparen {T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Relative Complement

{{:De Morgan's Laws (Set Theory)/Relative Complement/Complement of Intersection}}

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)/Set Complement

{{:De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection}}

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

{{:De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection}}

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

{{:De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection}}

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

{{:De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection}}

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}}
Theorem: Image of Set Difference under Mapping/Corollary 1

Let $f: S \to T$ be a mapping.
Let $S_1 \subseteq S_2 \subseteq S$.
Then:
:$\relcomp {f \sqbrk {S_2} } {f \sqbrk {S_1} } \subseteq f \sqbrk {\relcomp {S_2} {S_1} }$
where $\complement$ (in this context) denotes relative complement.

Proof:
From {{Corollary|Image of Set Difference under Relation|1}}:
:$\relcomp {\RR \sqbrk {S_2} } {\RR \sqbrk {S_1} } \subseteq \RR \sqbrk {\relcomp {S_2} {S_1} }$
where $\RR \subseteq S \times T$ is a relation on $S \times T$.
As $f$, being a mapping, is also a relation, it follows directly that:
:$\relcomp {f \sqbrk {S_2} } {f \sqbrk {S_1} } \subseteq f \sqbrk {\relcomp {S_2} {S_1} }$
{{qed}}
Category:Image of Set Difference under Mapping
c19w4yi9pvlwm2qlrvsgh9lvy67v37i