nyuuzyou/wikis huggingface dataset:
Powerset is not Subset of its Set/Proof 2

== Theorem ==
== Proof ==
 that $\powerset A \subseteq A$.
Let $I: \powerset A \to A$ be the identity mapping.
$I$ is an injection by Identity Mapping is Injection.
But by No Injection from Power Set to Set, this is a contradiction.
Category:Powerset is not Subset of its Set
Powerset of Subset is Closed under Intersection

== Theorem ==
Let $S$ be a set.
Let $T \subseteq S$ be a subset of $S$.
Let $\powerset S$ denote the power set of $S$.
Then $\powerset T$ is a closed subset of $\powerset S$ under set intersection:
:$\forall A, B \in \powerset T: A \cap B \in \powerset T$
== Proof ==
A direct application of Power Set is Closed under Intersection.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Exercise $8.3$
Category:Closed Algebraic Structures
Category:Power Set
Category:Set Intersection
Category:Subsets
Powerset of Subset is Closed under Symmetric Difference

== Theorem ==
Let $S$ be a set.
Let $T \subseteq S$ be a subset of $S$.
Let $\powerset S$ denote the power set of $S$.
Then $\powerset T$ is a closed subset of $\powerset S$ under set intersection:
:$\forall A, B \in \powerset T: A \symdif B \in \powerset T$
where $\symdif$ denotes symmetric difference.
== Proof ==
A direct application of Power Set is Closed under Symmetric Difference.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Exercise $8.3$
Category:Closed Algebraic Structures
Category:Power Set
Category:Symmetric Difference
Category:Subsets
Powerset of Subset is Closed under Union

== Theorem ==
Let $S$ be a set.
Let $T \subseteq S$ be a subset of $S$.
Let $\powerset S$ denote the power set of $S$.
Then $\powerset T$ is a closed subset of $\powerset S$ under set union:
:$\forall A, B \in \powerset T: A \cup B \in \powerset T$
== Proof ==
A direct application of Power Set is Closed under Union.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Exercise $8.3$
Category:Closed Algebraic Structures
Category:Power Set
Category:Set Union
Category:Subsets
Praeclarum Theorema

== Theorem ==
=== Formulation 1 ===
=== Formulation 2 ===
== Also see ==
Compare the Constructive Dilemma, which is similar in appearance.
== Historical Note ==
== Linguistic Note ==
== Sources ==
* 
Category:Praeclarum Theorema
Category:Conditional
Category:Conjunction
Category:Named Theorems
Praeclarum Theorema/Formulation 1

== Theorem ==
:$\paren {p \implies q} \land \paren {r \implies s} \vdash \paren {p \land r} \implies \paren {q \land s}$
== Proof 1 ==
== Proof by Truth Table ==
== Proof 3 ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Exercise $1 \ \text{(g)}$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.4: \ 2 \ \text{(g)}$
Category:Praeclarum Theorema
Praeclarum Theorema/Formulation 1/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen for all boolean interpretations by inspection, where the truth value under the main connective on the is $T$, that under the one on the is also $T$:
$\begin{array}{|ccccccc||ccccccc|} \hline
(p & \implies & q) & \land & (r & \implies & s) & (p & \land & r) & \implies & (q & \land & s) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \F & \T & \T & \F & \F & \F & \T & \F & \F & \T \\
\F & \T & \F & \F & \T & \F & \F & \F & \F & \T & \T & \F & \F & \F \\
\F & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \F & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \F & \T & \T & \F & \F & \F & \T & \T & \T & \T \\
\F & \T & \T & \F & \T & \F & \F & \F & \F & \T & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \F & \F & \T & \T & \T & \F & \F & \T & \F & \F & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \F & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
Hence the result.
Note that the two formulas are not equivalent, as the relevant columns do not match exactly.
Category:Truth Table Proofs
Category:Praeclarum Theorema
Praeclarum Theorema/Formulation 2

== Theorem ==
:$\vdash \paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} }$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$: Theorem $\text{T32}$
Category:Praeclarum Theorema
Praeclarum Theorema/Historical Note

== Historical Note on Praeclarum Theorema ==
The Praeclarum Theorema was noted and named by , who stated and proved it in the following manner:
:If $a$ is $b$ and $d$ is $c$, then $ad$ will be $bc$.
:This is a fine theorem, which is proved in this way:
:$a$ is $b$, therefore $ad$ is $bd$ (by what precedes),
:$d$ is $c$, therefore $bd$ is $bc$ (again by what precedes),
:$ad$ is $bd$, and $bd$ is $bc$, therefore $ad$ is $bc$. 
:Q.E.D.
== Sources ==
:(Leibniz, Logical Papers, p. 41).
* 1679 - 1686: : Addenda to the Specimen of the Universal Calculus: pp. $40 - 46$ 
Category:Historical Notes
Praeclarum Theorema for Meet Semilattices

== Theorem ==
Let $(S, \wedge, \preceq)$ be a meet semilattice.
Let $a, b, c, d \in S$.
Let $a \preceq b$.
Let $c \preceq d$.
Then $(a \wedge c) \preceq (b \wedge d)$.
== Proof ==
By Meet Semilattice is Ordered Structure, $\preceq$ is compatible with $\wedge$.
By the definition of ordering, $\preceq$ is transitive.
Thus the theorem holds by Operating on Transitive Relationships Compatible with Operation.
== Also See ==
* Praeclarum Theorema, an analogous result in logic
Category:Lattice Theory
Pratt's Lemma

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let:
:$\sequence {g_n}_{n \mathop \in \N}$
:$\sequence {G_n}_{n \mathop \in \N}$
:$\sequence {f_n}_{n \mathop \in \N}$
be sequences of $\mu$-integrable functions.
Let the pointwise limits:
:$\ds f := \lim_{n \mathop \to \infty} f_n$
:$\ds g := \lim_{n \mathop \to \infty} g_n$
:$\ds G := \lim_{n \mathop \to \infty} G_n$
exist.
Let $g$ and $G$ be $\mu$-integrable.
Suppose that, for all $x \in X$ and $n \in \N$:
:$\map {g_n} x \le \map {f_n} x \le \map {G_n} x$
Finally, suppose the following hold:
:$\ds \lim_{n \mathop \to \infty} \int g_n \rd \mu = \int g \rd \mu$
:$\ds \lim_{n \mathop \to \infty} \int G_n \rd \mu = \int G \rd \mu$
Then:
:$\ds \lim_{n \mathop \to \infty} \int f_n \rd \mu = \int f \rd \mu$
and the latter is finite.
== Proof ==
== Sources ==
* : $\S 11$: Problem $3$
Category:Measure Theory
Pre-Image Sigma-Algebra of Generated Sigma-Algebra

== Theorem ==
Let $f: X \to Y$ be a mapping.
Let $\GG \subseteq \powerset Y$ be a collection of subsets of $Y$.
Then the following equality of $\sigma$-algebras on $X$ holds:
:$f^{-1} \sqbrk {\map \sigma \GG} = \map \sigma {f^{-1} \sqbrk \GG}$
where
:$\sigma$ denotes a generated $\sigma$-algebra
:$f^{-1} \sqbrk {\map \sigma \GG}$ denotes the pre-image $\sigma$-algebra
:$f^{-1} \sqbrk \GG$ is the preimage of $\GG$ under $f$
== Proof ==
Since $\GG \subseteq \map \sigma \GG$, it follows immediately that:
:$f^{-1} \sqbrk \GG \subseteq f^{-1} \sqbrk {\map \sigma \GG}$
By Pre-Image Sigma-Algebra on Domain is Sigma-Algebra, the latter is a $\sigma$-algebra, and so by Generated Sigma-Algebra Preserves Subset, it follows that:
:$\map \sigma {f^{-1} \sqbrk \GG} \subseteq f^{-1} \sqbrk {\map \sigma \GG}$
Conversely, by definition of generated $\sigma$-algebra, we have:
:$f^{-1} \sqbrk \GG \subseteq \map \sigma {f^{-1} \sqbrk \GG}$
Hence from Mapping Measurable iff Measurable on Generator, it follows that $f$ is $\map \sigma {f^{-1} \sqbrk \GG} \, / \, \map \sigma \GG$-measurable.
But this by definition of measurable mapping means that:
:$f^{-1} \sqbrk {\map \sigma \GG} \subseteq \map \sigma {f^{-1} \sqbrk \GG}$
Hence the result, by definition of set equality.
== Sources ==
* : $\S 7$: Problem $8$
Category:Sigma-Algebras
Pre-Image Sigma-Algebra on Codomain is Sigma-Algebra

== Theorem ==
Let $X, X'$ be sets, and let $f: X \to X'$ be a mapping.
Let $\Sigma$ be a $\sigma$-algebra on $X$.
Denote with $\Sigma'$ the pre-image $\sigma$-algebra on the domain of $f$.
Then $\Sigma'$ is a $\sigma$-algebra on $X'$.
== Proof ==
Verify the axioms for a $\sigma$-algebra in turn:
=== Axiom $(\text {SA} 1)$ ===
As $f$ is a mapping, it is immediate that $f^{-1} \sqbrk {X'} = X$.
Also $X \in \Sigma$ as $\Sigma$ is a $\sigma$-algebra.
Hence $X' \in \Sigma'$.
=== Axiom $(\text {SA} 2)$ ===
Let $S' \in \Sigma'$.
By Preimage of Set Difference under Mapping and $f^{-1} \sqbrk {X'} = X$:
:$f^{-1} \sqbrk {X' \setminus S'} = f^{-1} \sqbrk {X'} \setminus f^{-1} \sqbrk {S'}$
Now $f^{-1} \sqbrk {X'} = X \in \Sigma$, and $f^{-1} \sqbrk {S'} \in \Sigma$ was already assumed.
As $\Sigma$ is a $\sigma$-algebra, it follows that $f^{-1} \sqbrk {X' \setminus S'} \in \Sigma$ as well.
Hence $X' \setminus S' \in \Sigma'$.
=== Axiom $(\text {SA} 3)$ ===
Let $\sequence {S'_i}_{i \mathop \in \N}$ be a sequence in $\Sigma'$.
By Preimage of Union under Mapping: General Result, have:
:$\ds f^{-1} \sqbrk {\bigcup_{i \mathop \in \N} S'_i} = \bigcup_{i \mathop \in \N} f^{-1} \sqbrk {S'_i}$
By assumption, $S'_i \in \Sigma'$ for all $i \in \N$; hence $f^{-1} \sqbrk {S'_i} \in \Sigma$ for all $i \in \N$.
Now $\ds \bigcup_{i \mathop \in \N} f^{-1} \sqbrk {S'_i} \in \Sigma$ as $\Sigma$ is a $\sigma$-algebra.
Hence $\ds \bigcup_{i \mathop \in \N} S'_i \in \Sigma'$.
== Sources ==
* : $\S 7$: Problem $2$
Category:Sigma-Algebras
Category:Examples of Sigma-Algebras
Pre-Image Sigma-Algebra on Domain is Generated by Mapping

== Theorem ==
Let $X, X'$ be sets, and let $f: X \to X'$ be a mapping.
Let $\Sigma'$ be a $\sigma$-algebra on $X'$.
Let $f: X \to X'$ be a mapping.
Then:
:$\map \sigma f = \map {f^{-1} } {\Sigma'}$
where
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$
:$\map {f^{-1} } {\Sigma'}$ denotes the pre-image $\sigma$-algebra under $f$
== Proof ==
By Characterization of Sigma-Algebra Generated by Collection of Mappings:
:$\map \sigma f = \map \sigma {\map {f^{-1} } {\Sigma'} }$
where the latter $\sigma$ denotes a $\sigma$-algebra generated by a collection of subsets.
By Pre-Image Sigma-Algebra on Domain is Sigma-Algebra, $\map {f^{-1} } {\Sigma'}$ is a $\sigma$-algebra.
Hence:
:$\map \sigma {\map {f^{-1} } {\Sigma'} } = \map {f^{-1} } {\Sigma'}$
== Sources ==
* : $\S 7$: Problem $3 \ \text{(i)}$
Category:Measure Theory
Pre-Image Sigma-Algebra on Domain is Sigma-Algebra

== Theorem ==
Let $X, X'$ be sets, and let $f: X \to X'$ be a mapping.
Let $\Sigma'$ be a $\sigma$-algebra on $X'$.
Then $f^{-1} \sqbrk {\Sigma'}$, the pre-image $\sigma$-algebra on the domain of $f$, is a $\sigma$-algebra on $X$.
== Proof ==
Verify the axioms for a $\sigma$-algebra in turn:
=== Axiom $(1)$ ===
As $f$ is a mapping, it is immediate that $f^{-1} \sqbrk {X'} = X$.
Also $X' \in \Sigma'$ as $\Sigma'$ is a $\sigma$-algebra.
Hence $X \in f^{-1} \sqbrk {\Sigma'}$.
=== Axiom $(2)$ ===
Let $S = f^{-1} \sqbrk {E'} \in f^{-1} \sqbrk {\Sigma'}$. 
By Preimage of Set Difference under Mapping and $f^{-1} \sqbrk {X'} = X$, have:
:$X \setminus S = f^{-1} \sqbrk {X'} \setminus f^{-1} \sqbrk {E'} = f^{-1} \sqbrk {X' \setminus E'}$
As $X' \setminus E' \in \Sigma'$, this means $X \setminus S \in f^{-1} \sqbrk {\Sigma'}$.
=== Axiom $(3)$ ===
Let $\sequence {S_i}_{i \mathop \in \N}$ be a sequence in $f^{-1} \sqbrk {\Sigma'}$.
Let, for all $i \in \N$, $E'_i \in \Sigma'$ such that $S_i = f^{-1} \sqbrk {E'}$.
By Preimage of Union under Mapping: General Result, have:
:$\ds \bigcup_{i \mathop \in \N} S_i = \bigcup_{i \mathop \in \N} f^{-1} \sqbrk {E'_i} = f^{-1} \sqbrk {\bigcup_{i \mathop \in \N} E'_i}$
Now $\ds \bigcup_{i \mathop \in \N} E'_i \in \Sigma'$ as $\Sigma'$ is a $\sigma$-algebra.
Hence $\ds \bigcup_{i \mathop \in \N} S_i \in f^{-1} \sqbrk {\Sigma'}$.
== Sources ==
* : $3.3 \ \text{(vii)}$, $\S 3$: Problem $2$
Category:Sigma-Algebras
Pre-Measure of Finite Stieltjes Function Extends to Unique Measure

== Theorem ==
Let $\JJ_{ho}$ denote the collection of half-open intervals in $\R$.
Let $f: \R \to \R$ be a finite Stieltjes function.
Then the pre-measure of $f$, $\mu_f$, extends uniquely to a measure $\mu$ on $\map \BB \R$, the Borel $\sigma$-algebra on $\R$.
This unique measure $\mu$ is the measure of $f$.
== Proof ==
We intend to use Carathéodory's Theorem (Measure Theory).
To this end, observe that by Characterization of Euclidean Borel Sigma-Algebra, we have:
:$\map \BB \R = \map \sigma {\JJ_{ho} }$
From Pre-Measure of Finite Stieltjes Function is Pre-Measure, $\mu_f$ is a pre-measure.
Note that for all $n \in \N$, we have:
:$\map {\mu_f} {\hointr {-n} n} = \map f n - \map f {-n} < +\infty$
and $\hointr {-n} n \uparrow \R$ as an increasing sequence of sets.
All these facts combine with Carathéodory's Theorem (Measure Theory) to establish existence and uniqueness of $\mu$.
== Sources ==
* : $\S 7$: Problem $9 \ \text{(ii)}$
Category:Pre-Measures
Category:Stieltjes Functions
Pre-Measure of Finite Stieltjes Function is Pre-Measure

== Theorem ==
Let $\JJ_{ho}$ denote the collection of half-open intervals in $\R$.
Let $f: \R \to \R$ be a finite Stieltjes function.
Then the pre-measure of $f$, $\mu_f: \JJ_{ho} \to \overline \R_{\ge 0}$ is a pre-measure.
Here, $\overline \R_{\ge 0}$ denotes the set of positive extended real numbers.
== Proof ==
It is immediate from the definition of $\mu_f$ that:
:$\map {\mu_f} \O = 0$
Now suppose that for some half-open interval $\hointr a b$ one has:
:$\ds \hointr a b = \bigcup_{n \mathop \in \N} \hointr {b_n} {b_{n + 1} }$
where $b_0 = a$ and $\ds \lim_{n \mathop \to \infty} b_n = b$.
Then we compute:
which verifies the second condition for a pre-measure.
Hence $\mu_f$ is indeed a pre-measure.
Category:Pre-Measures
Category:Stieltjes Functions
Preceding and Way Below implies Way Below

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $u, x, y, z \in S$ such that
:$u \preceq x \ll y \preceq z$
where $\ll$ denotes the way below relation.
Then
:$u \ll z$
== Proof ==
Let $D$ be a directed subset of $S$ such that
:$D$ admits a supremum
and
:$z \preceq \sup D$
By definition of transitivity:
:$y \preceq \sup D$
By definition of way below relation:
:$\exists d \in D: x \preceq d$
Thus by definition of transitivity:
:$\exists d \in D: u \preceq d$
Thus by definition of way below relation:
:$u \ll z$
== Sources ==
* 
* 
Category:Way Below Relation
Preceding iff Join equals Larger Operand

== Theorem ==
Let $\left({S, \preceq}\right)$ be a join semilattice.
Let $x, y \in S$.
Then
:$x \preceq y$ $x \vee y = y$
== Proof ==
=== Sufficient Condition ===
Let
:$x \preceq y$
By definition of join:
:$x \vee y = \sup \left\{ {x, y}\right\}$
By definitions of upper bound and reflexivity:
:$y$ is upper bound for $\left\{ {x, y}\right\}$
and
:$\forall z \in S: z$ is upper bound for $\left\{ {x, y}\right\} \implies y \preceq z$
Thus by definition of supremum:
:$y = \sup \left\{ {x, y}\right\} = x \vee y$
=== Necessary Condition ===
Let
:$x \vee y = y$
Thus by Join Succeeds Operands:
:$x \preceq y$
== Sources ==
* 
Category:Join and Meet
Category:Join and Meet Semilattices
Preceding iff Meet equals Less Operand

== Theorem ==
Let $\struct {S, \preceq}$ be a meet semilattice.
Let $x, y \in S$.
Then
:$x \preceq y$ $x \wedge y = x$
== Proof ==
=== Sufficient Condition ===
Let
:$x \preceq y$
By definition of meet:
:$x \wedge y = \inf \set {x, y}$
By definitions of lower bound and reflexivity:
:$x$ is lower bound for $\set {x, y}$
and
:$\forall z \in S: z$ is lower bound for $\set {x, y} \implies z \preceq x$
Thus by definition of infimum:
:$x = \inf \set {x, y} = x \wedge y$
=== Necessary Condition ===
Let
:$x \wedge y = x$
Thus by Meet Precedes Operands:
:$x \preceq y$
== Sources ==
* 
Category:Join and Meet
Category:Join and Meet Semilattices
Preceding implies Image is Subset of Image

== Theorem ==
Let $\struct {S, \precsim}$ be a preordered set.
Let $x, y \in S$ such that
:$x \precsim y$
Then $\map \precsim y \subseteq \mathord {\map \precsim x}$
where $\map \precsim y$ denotes the image of $y$ under $\precsim$.
== Proof ==
Let $z \in \mathord {\map \precsim y}$
By definition of image of element:
:$y \precsim z$
By definition of transitivity:
:$x \precsim z$
Thus by definition of image of element:
:$z \in \mathord {\map \precsim x}$
== Sources ==
* 
Category:Preorder Theory
Preceding implies Inclusion of Segments of Auxiliary Relation

== Theorem ==
Let $\left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Let $R$ be an auxiliary relation on $S$.
Let $x, y \in S$ such that
:$x \preceq y$
Then
:$x^R \subseteq y^R$
where $x^R$ denotes the $R$-segment of $x$.
== Proof ==
Let $a \in x^R$.
By definition of $R$-segment of $x$:
:$\left({a, x}\right) \in R$
By definition of reflexivity:
:$a \preceq a$
By definition of auxiliary relation:
:$\left({a, y}\right) \in R$
Thus by definition of $R$-segment of $y$:
:$a \in y^R$
== Sources ==
* 
* 
Category:Auxiliary Relations
Preceding implies Way Below Closure is Subset of Way Below Closure

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \preceq y$
Then $x^\ll \subseteq y^\ll$
where $x^\ll$ denotes the way below closure of $x$.
== Proof ==
Let $z \in x^\ll$.
By definition of way below closure:
:$z \ll x$
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$z \ll y$
Thus by definition of way below closure:
:$z \in y^\ll$
== Sources ==
* 
Category:Way Below Relation
Preceding implies if Less Upper Bound then Greater Upper Bound

== Theorem ==
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \preceq y$
Let $X \subseteq S$.
Then
:$x$ is upper bound for $X \implies y$ is upper bound for $X$
and
:$y$ is lower bound for $X \implies x$ is lower bound for $X$.
== Proof ==
=== First Implication ===
Let $x$ be upper bound for $X$,
Let $z \in X$.
By definition of upper bound:
:$z \preceq x$
Thus by definition of transitivity:
:$z \preceq y$
=== Second Implication ===
This follows by mutatis mutandis.
== Sources ==
* 
Category:Order Theory
Preceding is Approximating Relation

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Then $\preceq$ is an approximating relation on $S$.
== Proof ==
Let $x \in S$.
Define $\RR := \mathord\preceq$.
By definitions of lower closure of element and $\RR$-segment:
:$x^\preceq = x^\RR$
where:
:$x^\preceq$ denotes the lower closure of $x$
:$x^\RR$ denotes the $\RR$-segment of $x$
Thus by Supremum of Lower Closure of Element:
:$x = \map \sup {x^\preceq} = \map \sup {x^\RR}$
Hence $\preceq$ is an approximating relation on $S$.
== Sources ==
* 
* 
Category:Approximating Relations
Preceding is Auxiliary Relation

== Theorem ==
Let $\left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Then
:$\preceq$ is an auxiliary relation.
== Proof ==
:$\forall x, y \in S: x \preceq y \implies x \preceq y$
Then condition $(1)$ of auxiliary relation is satisfied.
By definition of transitivity:
:$\forall x, y, z, u \in S: x \preceq y \preceq z \preceq u \implies x \preceq u$
Then the condition $(2)$ of auxiliary relation is satisfied.
By definition of supremum:
:$\forall x, y, z \in S: x \preceq z \land y \preceq z \implies x \vee y \preceq z$
Then the condition $(3)$ of auxiliary relation is satisfied.
By definition of smallest element:
:$\forall x \in S: \bot \preceq x$
Then the condition $(4)$ of auxiliary relation is satisfied.
Thus the result by definition auxiliary relation.
== Sources ==
* 
* 
Category:Auxiliary Relations
Preceding is Top in Ordered Set of Auxiliary Relations

== Theorem ==
Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\map {\it Aux} L$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\it Aux} L, \precsim}$ be an ordered set
where $\precsim \mathop = \subseteq \restriction_{\map {\it Aux} L \times \map {\it Aux} L}$
Then
:$\preceq \mathop = \top_P$
where $\top_P$ denotes the greatest element in $P$.
== Proof ==
By Preceding is Auxiliary Relation:
:$\preceq \mathop \in \map {\it Aux} L$
By definition:
:$\preceq$ is lower bound for $\O$ in $P$
We will prove that:
:$\forall R \in \map {\it Aux} L: R$ is lower bound for $\O \implies R \mathop \precsim \preceq$
Let $R \in \map {\it Aux} L$
By condition $(i)$ of definition of auxiliary relation:
:$R \mathop \subseteq \preceq$
Thus by definition of $\precsim$:
:$R \mathop \precsim \preceq$
By definition of infimum:
:$\preceq \mathop = \inf_P \O$
Thus by Infimum of Empty Set is Greatest Element:
:$\preceq \mathop = \top_P$
== Sources ==
* 
* 
Category:Auxiliary Relations
Precession/Examples/Spinning Top

== Example of Precession ==
Consider the child's toy the $T$.
When $T$ is set in motion, it is often the case that the axis of $T$ is not vertical.
If that is the case, then the tip of the axis describes a circular path, which gives the motion of $T$ a "wobble".
This is caused by precession.
== Sources ==
* 
* 
Category:Examples of Precession
Precisely One Function in terms of And, Or and Not

== Theorem ==
Let $\map P {A, B, C}$ denote the precisely one function on the statements $A$, $B$ and $C$.
Then:
:$\map P {A, B, C} \dashv \vdash \paren {A \land \neg B \land \neg C} \lor \paren {\neg A \land B \land \neg C} \lor \paren {\neg A \land \neg B \land C}$
where:
:$\land$ denotes conjunction
:$\lor$ denotes disjunction
:$\neg$ denotes negation
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||ccccc|} \hline
P & (A & B & C) & (((A & \land & \neg & B) & \land & \neg & C) & \lor & ((\neg & A & \land & B) & \land & \neg & C)) & \lor & ((\neg & A & \land & \neg & B) & \land & C) \\
\hline
F & F & F & F & F & F & T & F & F & T & F & F & T & F & F & F & F & T & F & F & T & F & T & T & F & F & F \\
T & F & F & T & F & F & T & F & F & F & T & F & T & F & F & F & F & F & T & T & T & F & T & T & F & T & T \\
T & F & T & F & F & F & F & T & F & T & F & T & T & F & T & T & T & T & F & T & T & F & F & F & T & F & F \\
F & F & T & T & F & F & F & T & F & F & T & F & T & F & T & T & F & F & T & F & T & F & F & F & T & F & T \\
T & T & F & F & T & T & T & F & T & T & F & T & F & T & F & F & F & T & F & T & F & T & F & T & F & F & F \\
F & T & F & T & T & T & T & F & F & F & T & F & F & T & F & F & F & F & T & F & F & T & F & T & F & F & T \\
F & T & T & F & T & F & F & T & F & T & F & F & F & T & F & T & F & T & F & F & F & T & F & F & T & F & F \\
F & T & T & T & T & F & F & T & F & F & T & F & F & T & F & T & F & F & T & F & F & T & F & F & T & F & T \\
\hline
\end{array}$
== Sources ==
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic: Exercise $(6)$
Category:Precisely One Function
Predecessor Function is Primitive Recursive

== Theorem ==
The predecessor function $\operatorname{pred}: \N \to \N$ defined as:
:$\map {\operatorname{pred} } n = \begin{cases}
0 & : n = 0 \\
n-1 & : n > 0
\end{cases}$
is primitive recursive.
== Proof ==
We can use Primitive Recursion on One Variable to find $g: \N^2 \to \N$ and $h: \N \to \N$ such that:
:$\map h n = \begin{cases}
\map {\operatorname{zero} } n & : n = 0 \\
\map g {n - 1, \map h {n - 1} } & : n > 0 
\end{cases}
$
By setting:
:$\map g {n, m} = \map {\pr^2_1} {n, m}$
we see that setting $h = \operatorname{pred}$ fits the pattern.
We have that the $\pr^2_1$ and $\operatorname{zero}$ functions are basic primitive recursive functions.
Hence the result.
Category:Primitive Recursive Functions