avewright/proofwiki-math huggingface dataset:
Theorem: Transitive Closure of Set-Like Relation is Set-Like

Let $A$ be a class.
Let $\RR$ be a set-like endorelation on $A$.
Let $\RR^+$ be the transitive closure of $\RR$.
Then $\RR^+$ is also a set-like relation.

Proof:
Let $x \in A$.
Let $A'$ be the class of all subsets of $A$.
For each $s \in A'$, $\RR^{-1}$ is a subset of $A$.
Hence by Inverse Image of Set under Set-Like Relation is Set and the definition of endorelation:
:$\RR^{-1} \in A'$
Define a mapping $G: A' \to A'$ as:
:$\forall s \in A': \map G s = \map {\RR^{-1} } s$
Recursively define a mapping $f: \N \to A'$ as follows:
:$\map f n = \begin {cases} \set x & : n = 0 \\ \map G {\map f {n - 1} } & : n > 0 \end {cases}$
By the {{Axiom-link|Infinity}} and the {{Axiom-link|Replacement}}:
:$\map f \N$ is a set.
Thus by the {{Axiom-link|Unions|Class Theory}}:
:$\ds \bigcup \map f \N$ is a set.
Let $y \in \map {\paren {\RR^+}^{-1} } x$.
By the definition of transitive closure:
:for some $n \in \N_{>0}$ there are $a_0, a_1, \dots, a_n$ such that $y = a_0 \mathrel \RR a_1 \mathrel \RR \cdots \mathrel \RR a_n = x$.
{{explain|it's a finite sort of induction, and a simple and common pattern.}}
Then by induction (working from $n$ to $0$), $\ds a_n, a_{n - 1}, \dots, a_0 \in \bigcup \map f \N$.
As this holds for all such $y$:
:$\ds \map {\paren {\RR^+}^{-1} } x \subseteq \bigcup \map f \N$
By the {{Axiom-link|Specification|Classes}}:
:$\map {\paren {\RR^+}^{-1} } x$ is a set.
As this holds for all $x \in A$:
:$\RR^+$ is a set-like relation.
{{qed}}
Category:Set Theory
Category:Transitive Closures
l9wpoo1ghyova1pj294pfm01cboxyyq
Theorem: Relational Closure from Transitive Closure

Let $A$ be a set or class.
Let $\RR$ be a relation on $A$.
Let $\RR^+$ be the transitive closure of $\RR$.
Let $B \subseteq A$.
Let $B' = B \cup \inv {\paren {\RR^+} } B$.
Let $C$ be an $\RR$-transitive subset or subclass of $A$ such that $B \subseteq C$.
Then:
:$B'$ is $\RR$-transitive
:$B' \subseteq C$
:If $B$ is a set and $\RR$ is set-like then $B'$ is a set.
That is, $B'$ is the relational closure of $B$ under $\RR$.

Proof:
=== $B'$ is $\RR$-transitive ===
Let $x \in B'$ and $y \in A$, and let $y \mathrel \RR x$.
If $x \in B$, then by the definition of transitive closure:
:$y \mathrel {\RR^+} x$
so:
:$y \in B'$
Let $x \in \inv {\paren {\RR^+} } B$.
Then:
:$x \mathrel {\RR^+} b$
for some $b \in B$.
Since $\RR \subseteq \RR^+$, it follows that:
:$y \mathrel {\RR^+} x$
Since $\RR^+$ is transitive:
:$y \mathrel {\RR^+} b$
That is:
:$y \in \inv {\paren {\RR^+} } B$
so $y \in B'$.
As this holds for all such $x$ and $y$, $B'$ is $\RR$-transitive.
{{qed|lemma}}
Theorem: Minimal WRT Restriction

Let $A$ be a set or class.
Let $\RR$ be a relation on $A$.
Let $B$ be a subset or subclass of $A$.
Let $\RR'$ be the restriction of $\RR$ to $B$.
Let $m \in B$.
Then:
:$m$ is a strictly minimal element under $\RR$ in $B$
{{iff}}:
:$m$ is a strictly minimal element under $\RR'$ in $B$.

Proof:
=== Sufficient Condition ===
Let $m$ be a strictly minimal element under $\RR$ in $B$.
Let $x$ be any element of $B$.
{{AimForCont}} that $x \mathrel {\RR'} m$.
Then since $\RR' \subseteq \RR$:
:$x \mathrel \RR m$
contradicting the fact that $m$ is a strictly minimal element under $\RR$ in $B$.
Thus:
:$\lnot \paren {x \mathrel {\RR'} m}$
As this holds for all $x \in B$, $m$ is a strictly minimal element under $\RR'$ in $B$.
{{qed|lemma}}
Theorem: Intersection of Ordinals is Ordinal

Let $A$ be a non-empty class of ordinals.
Then its intersection $\bigcap A$ is an ordinal.

Proof:
Let $\alpha = \bigcap A$.
It will be demonstrated that $\alpha$ is an ordinal according to Definition $2$:
{{:Definition:Ordinal/Definition 2}}
Theorem: Meet with Complement is Bottom

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra, defined as in Definition 2.
Then:
:$\exists \bot \in S: \forall a \in S: a \wedge \neg a = \bot$
where $\wedge$ denotes the meet operation in $S$.
This element $\bot$ is unique for any given $S$, and is named '''bottom'''.

Proof:
Let $\exists r, s \in S: r \wedge \neg r = a, \ s \wedge \neg s = b$
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = r \wedge \neg r
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {s \wedge \neg s} \vee \paren {r \wedge \neg r}
      | c = {{Boolean-algebra-axiom|2|5}}
}}
{{eqn | r = \paren {r \wedge \neg r} \vee \paren {s \wedge \neg s}
      | c = {{Boolean-algebra-axiom|2|1}}
}}
{{eqn | r = s \wedge \neg s
      | c = {{Boolean-algebra-axiom|2|5}}
}}
{{eqn | r = b
      | c = {{hypothesis}}
}}
{{end-eqn}}
Thus, whatever $r$ and $s$ may be:
:$r \wedge \neg r = s \wedge \neg s$
This unique element can be assigned the symbol $\bot$ and named '''bottom''' as required.
{{qed}}
Theorem: Join with Complement is Top

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra, defined as in Definition 2.
Then:
:$\exists \top \in S: \forall a \in S: a \vee \neg a = \top$
where $\vee$ denotes the join operation in $S$.
This element $\top$ is unique for any given $S$, and is named '''top'''.

Proof:
Let $\exists r, s \in S: r \vee \neg r = a, \ s \vee \neg s = b$
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = r \vee \neg r
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {s \vee \neg s} \wedge \paren {r \vee \neg r}
      | c = {{Boolean-algebra-axiom|2|5}}
}}
{{eqn | r = \paren {r \vee \neg r} \wedge \paren {s \vee \neg s}
      | c = {{Boolean-algebra-axiom|2|1}}
}}
{{eqn | r = s \vee \neg s
      | c = {{Boolean-algebra-axiom|2|5}}
}}
{{eqn | r = b
      | c = {{hypothesis}}
}}
{{end-eqn}}
Thus, whatever $r$ and $s$ may be:
:$r \vee \neg r = s \vee \neg s$
This unique element can be assigned the symbol $\top$ and named '''top''' as required.
{{qed}}
Theorem: Equivalence of Definitions of Order Isomorphism

{{TFAE|def = Order Isomorphism}}
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.

Proof:
=== Definition 1 implies Definition 2 ===
Let $\phi: S \to T$ be an order isomorphism by Definition 1.
Then $\phi$ is bijective, and thus trivially surjective.
Let $x, y \in S$.
Then by Definition 1:
:$x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
Suppose that $\map \phi x \preceq_2 \map \phi y$.
Then by Definition 1:
:$\map {\phi^{-1} } {\map \phi x} \preceq_1 \map {\phi^{-1} } {\map \phi y}$
By the definition of inverse:
:$x \preceq_1 y$
Thus by Rule of Implication:
:$\map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$.
So:
:$x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
As this holds for all $x, y \in S$ and $\phi$ is surjective, $\phi$ is an order isomorphism by Definition 2.
{{qed|lemma}}
Theorem: Ordering is Equivalent to Subset Relation/Lemma

Let $\struct {S, \preceq}$ be an ordered set.
Then:
:$\forall a_1, a_2 \in S: \paren {a_1 \preceq a_2 \implies {a_1}^\preceq \subseteq {a_2}^\preceq}$
where ${a_1}^\preceq$ denotes the lower closure of $a_1$.

Proof:
Let $a_1 \preceq a_2$.
Then by the definition of lower closure:
:$a_1 \in {a_2}^\preceq$
Let $a_3 \in {a_1}^\preceq$.
Then by definition:
:$a_3 \preceq a_1$
As an ordering is transitive, it follows that:
:$a_3 \preceq a_2$
and so:
:$a_3 \in {a_2}^\preceq$
This holds for all $a_3 \in {a_1}^\preceq$.
Thus by definition of subset:
:${a_1}^\preceq \subseteq {a_2}^\preceq$
{{qed}}
Category:Ordering is Equivalent to Subset Relation
lo3iokpxebwwbe83j5i4rg6na5lviu8
Theorem: Smallest Element WRT Restricted Ordering

Let $S$ be a set or class.
Let $\preceq$ be an ordering on $S$.
Let $T$ be a subset or subclass of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Let $m \in T$.
Then $m$ is the $\preceq$-smallest element of $T$ {{iff}} $m$ is the $\preceq'$-smallest element of $T$.

Proof:
{{proof wanted|The same sort of utterly trivial thing as at Minimal WRT Restriction}}
Category:Smallest Elements
pk3bjqe63mj3zrgpqamspxwmg08vd65
Theorem: Restriction to Subset of Strict Total Ordering is Strict Total Ordering

Let $S$ be a set or class.
Let $\prec$ be a strict total ordering on $A$.
Let $T$ be a subset or subclass of $A$.
Then the restriction of $\prec$ to $B$ is a strict total ordering of $B$.

Proof:
Follows from:
:Restriction of Transitive Relation is Transitive
:Restriction of Antireflexive Relation is Antireflexive
:Restriction of Connected Relation is Connected
{{qed}}
Category:Total Orderings
i8o4agmo3vegz3a8i54osr3ngelqga6
Theorem: Restriction of Well-Founded Ordering is Well-Founded

Let $S$ be a set or class.
Let $T$ be a subset or subclass of $S$.
Let $\preceq$ be a well-founded ordering of $A$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then $\preceq'$ is a well-founded ordering of $T$.

Proof:
By Restriction of Ordering is Ordering, $\preceq'$ is an ordering.
By Restriction of Well-Founded Relation is Well-Founded, $\preceq'$ is a well-founded relation on $T$.
Hence the result by definition of well-founded ordering.
{{qed}}
Category:Order Theory
Category:Well-Founded Relations
gt3s509f9og72gfyqzi18hpu9x2ezcf
Theorem: Restriction of Well-Ordering is Well-Ordering

Let $S$ be a set or class.
Let $\preceq$ be a well-ordering of $S$.
Let $T$ be a subset or subclass of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then $\preceq'$ is a well-ordering of $T$.

Proof:
By the definition of well-ordering, $\preceq$ is a well-founded total ordering.
By Restriction of Total Ordering is Total Ordering, $\preceq'$ is a total ordering.
By Restriction of Well-Founded Ordering is Well-Founded, $\preceq'$ is a well-founded ordering.
Thus $\preceq'$ is a well-ordering.
{{qed}}
Category:Well-Orderings
3kosto3wuouy4edxrlyafvn9cj1d4rf
Theorem: Event Space contains Sample Space

:$\Omega \in \Sigma$

Proof:
{{begin-eqn}}
{{eqn | l = \Sigma
      | o = \ne
      | r = \O
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 1)$}}
}}
{{eqn | ll= \leadsto
      | q = \exists A
      | l = A 
      | o = \in
      | r = \Sigma
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadsto
      | l = \Omega \setminus A
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 2)$}}
}}
{{eqn | ll= \leadsto
      | l = A \cup \paren {\Omega \setminus A}
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 3)$}}
}}
{{eqn | ll= \leadsto
      | l = \Omega
      | o = \in
      | r = \Sigma
      | c = Union with Relative Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Event Space contains Empty Set

:$\O \in \Sigma$

Proof:
{{begin-eqn}}
{{eqn | l = \Sigma
      | o = \ne
      | r = \O
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 1)$}}
}}
{{eqn | ll= \leadsto
      | q = \exists A
      | l = A 
      | o = \in
      | r = \Sigma
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadsto
      | l = A \setminus A
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 2)$}}
}}
{{eqn | ll= \leadsto
      | l = \O
      | o = \in
      | r = \Sigma
      | c = Set Difference with Self is Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Power Set of Sample Space is Event Space

Let $\EE$ be an experiment whose sample space is $\Omega$.
Let $\powerset \Omega$ be the power set of $\Omega$.
Then $\powerset \Omega$ is an event space of $\EE$.

Proof:
Let $\powerset \Omega := \Sigma$.
;Event Space Axiom $(\text {ES} 1)$:
From Empty Set is Subset of All Sets we have that $\O \subseteq \Omega$.
By the definition of power set:
:$\O \in \Sigma$
thus fulfilling axiom $(\text {ES} 1)$.
{{qed|lemma}}
;Event Space Axiom $(\text {ES} 2)$:
Let $A \in \Sigma$.
Then by the definition of power set:
:$A \subseteq \Omega$
From Set with Relative Complement forms Partition:
:$\Omega \setminus A \subseteq \Omega$
and so by the definition of power set:
:$\Omega \setminus A \in \Sigma$
thus fulfilling axiom $(\text {ES} 2)$.
{{qed|lemma}}
;Event Space Axiom $(\text {ES} 3)$:
Let $\sequence {A_i}$ be a countably infinite sequence of sets in $\Sigma$.
Then from Power Set is Closed under Countable Unions:
:$\ds \bigcup_{i \mathop \in \N} A_i \in \Sigma$
thus fulfilling axiom $(\text {ES} 3)$.
{{qed|lemma}}
All the event space axioms are seen to be fulfilled by $\powerset \Omega$.
Hence the result.
{{qed}}
Theorem: Power Set of Sample Space is Event Space

Let $\EE$ be an experiment whose sample space is $\Omega$.
Let $\powerset \Omega$ be the power set of $\Omega$.
Then $\powerset \Omega$ is an event space of $\EE$.

Proof:
For $\powerset \Omega$ to be an event space of $\EE$, it needs to fulfil the following properties:
:$(1): \quad \powerset \Omega \ne \O$, that is, an event space can not be empty.
:$(2): \quad$ If $A \in \powerset \Omega$, then $\relcomp \Omega A \in \powerset \Omega$, that is, the complement of $A$ relative to $\Omega$, is also in $\powerset \Omega$.
:$(3): \quad$ If $A_1, A_2, \ldots \in \powerset \Omega$, then $\ds \bigcup_{i \mathop = 1}^\infty A_i \in \powerset \Omega$, that is, the union of any countable collection of elements of $\powerset \Omega$ is also in $\powerset \Omega$.
These all follow directly from Power Set is Sigma-Algebra.
{{qed}}
Theorem: Event Space from Single Subset of Sample Space

Let $\EE$ be an experiment whose sample space is $\Omega$.
Let $\O \subsetneqq A \subsetneqq \Omega$.
Then $\Sigma := \set {\O, A, \Omega \setminus A, \Omega}$ is an event space of $\EE$.

Proof:
;Event Space Axiom $(\text {ES} 1)$:
From its definition:
:$\Sigma \ne \O$
thus fulfilling axiom $(\text {ES} 1)$.
{{qed|lemma}}
;Event Space Axiom $(\text {ES} 2)$:
From Set Difference with Empty Set is Self:
:$\Omega \setminus \O = \Omega \in \Sigma$
From Set Difference with Self is Empty Set:
:$\Omega \setminus \Omega = \O \in \Sigma$
By definition:
:$\Omega \setminus A \in \Sigma$
From Relative Complement of Relative Complement:
:$\Omega \setminus \paren {\Omega \setminus A} = A \in \Sigma$
Thus axiom $(\text {ES} 2)$ is fulfilled.
{{qed|lemma}}
;Event Space Axiom $(\text {ES} 3)$:
From Union with Empty Set:
:$\forall X \in \Sigma: X \cup \O = X \in \Sigma$
From Union with Superset is Superset:
:$\forall X \in \Sigma: X \cup \Sigma = \Sigma \in \Sigma$
From Set Union is Idempotent:
:$\forall X \in \Sigma: X \cup X = X \in \Sigma$
From Union with Relative Complement:
:$A \cup \paren {\Omega \setminus A} = \Sigma \in \Sigma$
It follows that axiom $(\text {ES} 3)$ is fulfilled.
{{qed}}
Theorem: Intersection of Events is Event

:$A, B \in \Sigma \implies A \cap B \in \Sigma$

Proof:
{{begin-eqn}}
{{eqn | l = A, B
      | o = \in
      | r = \Sigma
      | c=
}}
{{eqn | ll= \leadsto
      | l = \Omega \setminus A, \ \Omega \setminus B
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 2)$}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\Omega \setminus A} \cup \paren {\Omega \setminus A}
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 3)$}}
}}
{{eqn | ll= \leadsto
      | l = \Omega \setminus \paren {A \cap B}
      | o = \in
      | r = \Sigma
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | ll= \leadsto
      | l = \Omega \setminus \paren {\Omega \setminus \paren {A \cap B} }
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 2)$}}
}}
{{eqn | ll= \leadsto
      | l = A \cap B
      | o = \in
      | r = \Sigma
      | c = Relative Complement of Relative Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference of Events is Event

:$A, B \in \Sigma \implies A \setminus B \in \Sigma$

Proof:
{{begin-eqn}}
{{eqn | l = A, B
      | o = \in
      | r = \Sigma
      | c=
}}
{{eqn | ll= \leadsto
      | l = A, \Omega \setminus B
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 2)$}}
}}
{{eqn | ll= \leadsto
      | l = A \cap \paren {\Omega \setminus B}
      | o = \in
      | r = \Sigma
      | c = Intersection of Events is Event
}}
{{eqn | ll= \leadsto
      | l = A \setminus B
      | o = \in
      | r = \Sigma
      | c = Set Difference as Intersection with Relative Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Composition of Affine Transformations is Affine Transformation

Let $\EE$, $\FF$ and $\GG$ be affine spaces with difference spaces $E$, $F$ and $G$ respectively.
Let $\LL: \EE \to \FF$ and $\MM: \FF \to \GG$ be affine transformations.
Let $L$ and $M$ be the tangent maps of $\LL$ and $\MM$ respectively.
Then the composition $\MM \circ \LL: \EE \to \FF$ is an affine transformation with tangent map $M \circ L$.

Proof:
Let $\NN = \MM \circ \LL : \EE \to \GG$ be the composition.
We want to show that for any $p, q \in \EE$
:$\map \GG Q = \map \GG p + \map {M \circ L} {\vec {p q} }$
We find that:
{{begin-eqn}}
{{eqn | l = \map \GG q
      | r = \map {\MM \circ \LL} q
}}
{{eqn | r = \map \MM {\map \LL p} + \map L {\vec{p q} }
      | c = $\LL$ is an Affine Transformation
}}
{{end-eqn}}
Now let:
:$p' = \map \LL p$
and:
:$q' = \map \LL p + \map L {\vec {p q} }$
so:
:$\vec {p' q'} = \map L {\vec {p q} }$
Then:
{{begin-eqn}}
{{eqn | l = \map \GG q
      | r = \map \MM {q'}
}}
{{eqn | r = \map \MM {p'} + \map M {\vec {p' q'} }
      | c = $\MM$ is an Affine Transformation
}}
{{eqn | r = \map \MM {\map \LL p} + \map M {\map L {\vec {p q} } }
      | c = Definitions of $p'$ and $q'$
}}
{{eqn | r = \map {\MM \circ \LL} p + \map {M \circ L} {\vec {p q} }
      | c = 
}}
{{end-eqn}}
as required.
{{Qed}}
Category:Affine Geometry
Category:Composite Mappings
31zq54mx30f8dqen3cjpq0zr4ipd6ui
Theorem: Symmetric Difference of Events is Event

:$A, B \in \Sigma \implies A \ast B \in \Sigma$

Proof:
{{begin-eqn}}
{{eqn | l = A, B
      | o = \in
      | r = \Sigma
      | c=
}}
{{eqn | ll= \leadsto
      | l = A \cup B
      | o = \in
      | r = \Sigma
      | c = {{Defof|Event Space|Event Space: Axiom $(\text {ES} 3)$}}
}}
{{eqn | lo= \land
      | l = A \cap B
      | o = \in
      | r = \Sigma
      | c = Intersection of Events is Event
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cup B} \setminus \paren {A \cap B}
      | o = \in
      | r = \Sigma
      | c = Set Difference of Events is Event
}}
{{eqn | ll= \leadsto
      | l = A \ast B
      | o = \in
      | r = \Sigma
      | c = {{Defof|Symmetric Difference|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Affine Transformations

Let $\EE$ and $\FF$ be affine spaces over a field $K$.
Let $\LL: \EE \to \FF$ be a mapping.
Then $\LL$ is an affine transformation {{iff}}:
:$\forall p, q \in \EE: \forall \lambda \in K: \map \LL {\lambda p + \paren {1 - \lambda} q} = \lambda \map \LL p + \paren {1 - \lambda} \map \LL q$
where $\lambda p + \paren {1 - \lambda} q$ and $\lambda \map \LL p + \paren {1 - \lambda} \map \LL q$ denote barycenters.

Proof:
=== Sufficient Condition ===
Let $\LL$ be an affine transformation.
Let $L$ be the tangent map.
Let $r \in \EE$ be any point.
Then by definition we have:
:$\lambda p + \paren {1 - \lambda} q = r + \lambda \vec{r p} + \paren {1 - \lambda} \vec{r q}$
Thus we find:
{{begin-eqn}}
{{eqn | l = \map \LL {\lambda p + \paren {1 - \lambda} q}
      | r = \map \LL r + \map L {\lambda p + \paren {1 - \lambda} q}
      | c = {{Defof|Affine Transformation}}
}}
{{eqn | r = \map \LL r + \lambda \map L p + \paren {1 - \lambda} \map L q
      | c = since $L$ is linear
}}
{{eqn | r = \lambda \map \LL p + \paren {1 - \lambda} \map \LL q
      | c ={{Defof|Barycenter}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Probability of Empty Event is Zero

:$\map \Pr \O = 0$

Proof:
From the conditions for $\Pr$ to be a probability measure, we have:
:$(1): \quad \forall A \in \Sigma: 0 \le \map \Pr A$
:$(2): \quad \map \Pr \Omega = 1$
:$(3): \quad \ds \map \Pr {\bigcup_{i \mathop \ge 1} A_i} = \sum_{i \mathop \ge 1} \map \Pr {A_i}$ where all $A_i$ are pairwise disjoint.
From the definition of event space, we have:
:$\Omega \in \Sigma$
:$A \in \Sigma \implies \relcomp \Omega A \in \Sigma$
From Intersection with Empty Set:
:$\O \cap \Omega = \O$
Therefore $\O$ and $\Omega$ are pairwise disjoint.
From Union with Empty Set:
:$\O \cup \Omega = \Omega$
Therefore we have:
{{begin-eqn}}
{{eqn | l = \map \Pr \Omega
      | r = \map \Pr {\O \cup \Omega}
      | c = 
}}
{{eqn | r = \map \Pr \O + \map \Pr \Omega
      | c = 
}}
{{end-eqn}}
As $\map \Pr \Omega = 1$, it follows that $\map \Pr \O = 0$.
{{qed}}
Theorem: Ordinal Membership is Asymmetric

Let $m$ and $n$ be ordinals.
Then it is not the case that $m \in n$ and $n \in m$.

Proof:
{{AimForCont}} $m \in n$ and $n \in m$.
Since $m$ is an ordinal, it is transitive.
Thus since $m \in n$ and $n \in m$, it follows that $m \in m$.
But this contradicts Ordinal is not Element of Itself.
{{qed}}
Category:Ordinals
oapnhc6j5eyfppc6gujiamnal6c9qm9
Theorem: Intersection of Ordinals is Smallest

Let $A$ be a non-empty set or class of ordinals.
Let $m = \bigcap A$ be the intersection of all the elements of $A$.
Then $m$ is the smallest element of $A$.

Proof:
By Intersection of Ordinals is Ordinal, $m$ is an ordinal.
By Intersection is Largest Subset, $m \subseteq a$ for each $a \in A$.
It remains to show that $m \in A$.
Let $m^+ = m \cup \set m$ be the successor of $m$.
By Relation between Two Ordinals:
:for each $a \in A$, either $m^+ \subseteq a$ or $a \in m^+$.
Let $m^+ \subseteq a$ for all $a \in A$.
Then by Intersection is Largest Subset $m^+ \subseteq m$.
This contradicts the fact that Ordinal is not Element of Itself.
Thus there is an $a \in A$ such that $a \in m^+$.
Thus $a \in m$ or $a = m$.
Let $a \in m$.
Then $a \subsetneqq m$.
This contradicts the fact that $m \subseteq a$.
Thus $a = m$.
Thus it follows that $m \in A$.
{{qed}}
Category:Ordinals
27ffaqxp1k494b4ndklpntimdi8l86v
Theorem: Class of All Ordinals is Well-Ordered by Subset Relation

Let $\On$ be the class of all ordinals.
Then the restriction of the subset relation, $\subseteq$, to $\On$ is a well-ordering.
That is:
:$\subseteq$ is an ordering on $\On$.
:If $A$ is a non-empty subclass of $\On$, then $A$ has a smallest element under the subset relation.

Proof:
By Subset Relation on Class is Ordering, $\subseteq$ is an ordering of any class.
Let $A$ be a subclass of $\On$.
By Intersection of Ordinals is Smallest, $A$ has a smallest element under the subset relation.
{{qed}}
Theorem: Class of All Ordinals is Well-Ordered by Subset Relation

Let $\On$ be the class of all ordinals.
Then the restriction of the subset relation, $\subseteq$, to $\On$ is a well-ordering.
That is:
:$\subseteq$ is an ordering on $\On$.
:If $A$ is a non-empty subclass of $\On$, then $A$ has a smallest element under the subset relation.

Proof:
From Class of All Ordinals is $g$-Tower, $\On$ is a $g$-tower.
The result follows from $g$-Tower is Well-Ordered under Subset Relation.
{{qed}}
Theorem: Subset is Compatible with Ordinal Successor

Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.
Let $x \in y$.
Then:
:$x^+ \in y^+$

Proof:
{{begin-eqn}}
{{eqn|l = x \in y
     |o = \implies
     |r = x \ne y
     |c = No Membership Loops
}}
{{eqn|o = \implies
     |r = x^+ \ne y^+
     |c = Equality of Successors
}}
{{eqn|l = x \in y
     |o = \implies
     |r = y \notin x
     |c = No Membership Loops
}}
{{eqn|o = \implies
     |r = y \notin x^+
     |c = $x ≠ y$ and {{Defof|Successor Set}}
}}
{{eqn|l = y^+ \in x^+
     |o = \implies
     |r = y \in x^+
     |c = Successor Set of Ordinal is Ordinal, Ordinals are Transitive, and Set is Element of Successor
}}
{{end-eqn}}
The last part is a contradiction, so $y^+ \notin x^+$.
By Ordinal Membership is Trichotomy:
:$x^+ \in y^+$
{{qed}}