avewright/proofwiki-math huggingface dataset:
Theorem: Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice/Lemma 1

Let $\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2}$.
Then:
:$x_1 \preccurlyeq_1 y_1$

Proof:
Recall the definition of lexicographic order:
{{:Definition:Lexicographic Order}}
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x_1, x_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1, y_2}
      | c = {{Defof|Upper Bound of Set}}
}}
{{eqn | ll= \leadsto
      | l = x_1
      | o = \prec_1
      | r = y_1
      | c = {{Defof|Lexicographic Order}}
}}
{{eqn | lo= \lor
      | l = \leftparen {x_1 = y_1}
      | o = \land
      | r = \rightparen {x_2 \preccurlyeq_2 y_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | o = \prec_1
      | r = y_1
      | c = 
}}
{{eqn | lo= \lor
      | l = x_1
      | r = y_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | o = \preccurlyeq_1
      | r = y_1
      | c = Definition of $\preccurlyeq_1$
}}
{{end-eqn}}
{{qed}}
Category:Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice
dssgzwbp2dfbh7b4unnbgrqoe6u6jzh
Theorem: Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice/Lemma 2

Let $x_1$ and $y_1$ be non-comparable elements in $S_1$:
:$\lnot \paren {x_1 \preccurlyeq_1 y_1}$ and $\lnot \paren {y_1 \preccurlyeq_1 x_1}$
Then $\tuple {x_1, x_2}$ and $\tuple {y_1, y_2}$ are non-comparable elements in $S_1 \times S_2$:
:$\lnot \paren {\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2} }$ and $\lnot \paren {\tuple {y_1, y_2} \preccurlyeq_l \tuple {x_1, x_2} }$

Proof:
Suppose $x_1$ and $y_1$ are non-comparable elements in $S_1$:
:$\lnot \paren {x_1 \preccurlyeq_1 y_1}$ and $\lnot \paren {y_1 \preccurlyeq_1 x_1}$
{{AimForCont}} that:
:$\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2}$ or $\tuple {y_1, y_2} \preccurlyeq_l \tuple {x_1, x_2}$
Then from Lemma $1$:
:$x_1 \preccurlyeq_1 y_1$ or $y_1 \preccurlyeq_1 x_1$
This contradicts our assumption.
Hence the result by Proof by Contradiction.
{{qed}}
Category:Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice
4tr3cxdbz26l7quvqrr2seuyxzpke0q
Theorem: Ordering is Directed iff Composite with Inverse is Trivial Ordering

Let $\struct {S, \RR}$ be an ordered set.
Then $\RR$ is a '''directed ordering''' {{iff}}:
:$\RR^{-1} \circ \RR = S \times S$
where:
:$\circ$ denotes composite relation
:$\RR^{-1}$ denotes inverse relation
:$S \times S$ denotes the trivial relation, that is, the Cartesian product of $S$ with itself.

Proof:
We are given that $\RR$ is an ordering.
Theorem: Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice/Corollary

Let $\struct {S_2, \preccurlyeq_2}$ have neither a greatest element nor a smallest element.
Then:
:$\preccurlyeq_l$ is a lattice ordering
{{iff}}:
:$\preccurlyeq_1$ is a total ordering
and:
:$\preccurlyeq_2$ is a lattice ordering.

Proof:
=== Sufficient Condition ===
Let $\preccurlyeq_l$ be a lattice ordering.
We are given that $\struct {S_2, \preccurlyeq_2}$ has neither a greatest element nor a smallest element.
From Condition $(2)$ of Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice, it follows that $\preccurlyeq_1$ is a total ordering.
Because $\struct {S_2, \preccurlyeq_2}$ has no smallest element, it follows from Condition $(4)$ of Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice that every doubleton subset of $S_2$ admits a supremum.
Because $\struct {S_2, \preccurlyeq_2}$ has no greatest element, it follows from Condition $(5)$ of Conditions for Lexicographic Order on Pair of Ordered Sets to be Lattice that every doubleton subset of $S_2$ admits an infimum.
Thus every doubleton subset of $S_2$ admits a supremum and an infimum.
That is, $\preccurlyeq_2$ is a lattice ordering.
{{qed|lemma}}
Theorem: Ordered Set of All Mappings is Lattice iff Codomain is Lattice or Domain is Empty

Let $S$ be a set.
Let $\struct {T, \preccurlyeq}$ be an ordered set.
Let $\struct {T^S, \preccurlyeq}$ denote the ordered set of all mappings from $S$ to $T$.
Then:
:$\struct {T^S, \preccurlyeq}$ is a lattice
{{iff}} either:
:$\struct {T, \preccurlyeq}$ is a lattice
or:
:$S = \O$

Proof:
Recall the definition of lattice:
{{:Definition:Lattice (Ordered Set)}}
First a lemma to take care of the case where $S = \O$:
Theorem: Condition for Ordered Set of All Mappings to be Total Ordering

Let $S$ be a set.
Let $\struct {T, \preccurlyeq}$ be an ordered set.
Let $\struct {T^S, \preccurlyeq}$ denote the ordered set of all mappings from $S$ to $T$.
Then:
:$\struct {T^S, \preccurlyeq}$ is a totally ordered set
{{iff}}:
:$\card S \le 1$
or:
:$\card T \le 1$

Proof:
=== Sufficient Condition ===
Let  $\struct {T^S, \preccurlyeq}$ be a totally ordered set.
Let $f, g \in T^S$ be arbitrary.
Let $S$ and $T$ be such that:
{{begin-eqn}}
{{eqn | q = \exists a, b \in S
      | l = a
      | o = \ne
      | r = b
}}
{{eqn | q = \exists x, y \in T
      | l = x
      | o = \ne
      | r = y
}}
{{end-eqn}}
Let $f: S \to T$ be defined as:
{{begin-eqn}}
{{eqn | r = x
      | l = \map f a
}}
{{eqn | r = y
      | l = \map f b
}}
{{eqn | r = y
      | l = \map g a
}}
{{eqn | r = x
      | l = \map g b
}}
{{end-eqn}}
As $\struct {T^S, \preccurlyeq}$ is a totally ordered set, either $f \preccurlyeq g$ or $g \preccurlyeq f$.
Suppose $f \preccurlyeq g$.
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = \map f a
      | o = \preccurlyeq
      | r = \map g a
      | c = 
}}
{{eqn | lo= 
      | l = \map f b
      | o = \preccurlyeq
      | r = \map g b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \preccurlyeq
      | r = x
      | c = 
}}
{{end-eqn}}
As $x \ne y$ this shows that $\preccurlyeq$ is not antisymmetric on $T$.
This contradicts the assumption that $\struct {T, \preccurlyeq}$ is an ordered set.
Hence if both $\card T > 1$ and $\card S > 1$ it cannot be the case that $\struct {T^S, \preccurlyeq}$ is a totally ordered set.
Thus by the Rule of Transposition, either $\card T \le 1$ or $\card S \le 1$.
{{finish}}
Theorem: Natural Numbers with Divisor Operation is Isomorphic to Subgroups of Integer Multiples under Inclusion

Let $\N_{>0}$ denote the set of strictly positive natural numbers.
For $n \in \N_{>0}$, let $n \Z$ denote the set of integer multiples of $n$.
Let $\struct {\Z, +}$ denote the additive group of integers.
Let $\mathscr G$ be the set of all subgroups of $\struct {\Z, +}$.
Consider the algebraic structure $\struct {\N_{>0}, \divides}$, where $\divides$ denotes the divisor operator:
:$a \divides b$ denotes that $a$ is a divisor of $b$
Let $\phi: \struct {\N_{>0}, \divides} \to \struct {\mathscr G, \supseteq}$ be the mapping defined as:
:$\forall n \in \N_{>0}: \map \phi n = n \Z$
Then $\phi$ is an order isomorphism.

Proof:
We note that from Subgroups of Additive Group of Integers, the subgroups of $\struct {\Z, +}$ are precisely the sets of integer multiples $n \Z$, for $n \in \N_{>0}$.
For each $n \in \N_{>0}$, there is a unique $n \Z \in \mathscr G$.
Hence $\phi$ is a bijection.
It remains to be demonstrated that $\phi$ is order-preserving in both directions.
Thus:
{{begin-eqn}}
{{eqn | l = a
      | o = \divides
      | r = b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists k \in \Z
      | l = k a
      | r = b
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = b \Z
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists m \in \Z
      | l = x
      | r = m b
      | c = {{Defof|Set of Integer Multiples}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists k \in \Z
      | l = x
      | r = \paren {m k} a
      | c = {{apriori}}: $k a = b$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = a \Z
      | c = {{Defof|Set of Integer Multiples}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a \Z
      | o = \supseteq
      | r = b \Z
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Subset of Join Semilattice on Total Ordering is Closed

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $\struct {S, \vee, \preccurlyeq}$ be the join semilattice with respect to $\preccurlyeq$.
Let $T \subseteq S$ be an arbitrary subset of $S$.
Then $\struct {T, \vee, \preccurlyeq}$ is closed under $\vee$.

Proof:
Let $x \in T$.
Then from Supremum of Singleton:
:$\sup \set x = x$
That is:
:$x \vee x = x$
and so:
:$x \vee x \in T$
Let $x, y \in T$.
From Supremum of Doubleton in Totally Ordered Set:
:$\sup \set {x, y} \in \set {x, y}$
That is:
:$x \vee y \in \set {x, y}$
But:
:$\set {x, y} \subseteq T$
Hence by definition of subset:
:$x \vee y \in T$
That is:
:$\struct {T, \vee, \preccurlyeq}$ is closed under $\vee$.
{{qed}}
Theorem: Supremum of Doubleton in Totally Ordered Set

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $D = \set {a, b} \subseteq S$ be an arbitrary doubleton subset of $S$.
Then:
:$\map \sup D \in D$
where $\sup D$ denotes the supremum of $D$.

Proof:
Let $D = \set {a, b} \subseteq S$ as asserted.
As $S$ is a totally ordered set, either $a \preccurlyeq b$ or $b \preccurlyeq a$.
{{WLOG}} let $a \preccurlyeq b$.
We have by definition of supremum that:
:$\forall x \in D: x \preccurlyeq \map \sup D$
:$\forall y \in S:$ if $y$ is an upper bound of $D$, then $\map \sup D \preccurlyeq y$.
Now we have:
:$\forall x \in D: x \preccurlyeq b$
Let $y \in S$ be an upper bound of $D$.
Then:
:$\forall x \in D: x \preccurlyeq y$
In particular:
:$b \preccurlyeq y$
Hence by definition:
:$\map \sup D = b$
Similarly, if $b \preccurlyeq a$, then {{mutatis}}:
:$\map \sup D = a$
In either case:
:$\map \sup D \in D$
{{qed}}
Category:Suprema
Category:Doubletons
9c5pvvp9t2lbphuxlo7j435dywe1r54
Theorem: Total Semilattice has Unique Total Ordering

Let $\struct {S, \vee}$ be a total semilattice.
There exists a unique total ordering $\preccurlyeq$ on $S$ such that:
:$x \vee y = \max \set {x, y}$
where:
:$\max \set {x, y} := \begin {cases} b & : a \preccurlyeq b \\ a & : b \preccurlyeq a \end {cases}$

Proof:
Recall the definition of total semilattice:
A '''total semilattice''' $\struct {S, \odot}$ is a '''semilattice''' which has the property that every subset of $\struct {S, \odot}$ is a '''subsemilattice'''.
That is, such that every subset of $\struct {S, \odot}$ is closed under $\odot$.
Let us define a relation $\RR$ on $S$ as:
:$\forall x, y \in S: x \mathrel \RR y \iff x \vee y = y$
It is to be shown that $\RR$ is a total ordering.
From Semilattice Induces Ordering, we have that $\RR$ is an ordering.
{{qed|lemma}}
Theorem: Semilattice has Unique Ordering such that Operation is Supremum

Let $\struct {S, \vee}$ be a semilattice.
Then there exists a unique ordering $\preccurlyeq$ on $S$ such that:
:$x \vee y = \sup \set {x, y}$
where $\sup \set {x, y}$ is the supremum of $\set {x, y}$ {{WRT}} $\preccurlyeq$.

Proof:
Let us define a relation $\RR$ on $S$ as:
:$\forall x, y \in S: x \mathrel \RR y \iff x \vee y = y$
From Semilattice Induces Ordering, we have that $\RR$ is an ordering.
Let us denote this ordering by $\preccurlyeq$, and recall its definition:
:$x \vee y = y \iff x \preccurlyeq y$
Theorem: Max Operation is Idempotent

The max operation operation is idempotent:
:$\map \max {x, x} = x$

Proof:
Follows immediately from the definition of max operation:
:$\map \max {a, b} = \begin {cases} b & : a \le b \\ a & : b \le a \end {cases}$
Setting $x = a = b$ returns the result.
{{Qed}}
Theorem: Natural Numbers under Min Operation forms Total Semilattice

Let $\struct {\N, \wedge}$ denote the set of natural numbers $\N$ under the min operation:
:$\forall a, b \in \N: a \wedge b := \min \set {a, b}$
Then $\struct {\N, \wedge}$ forms a total semilattice.

Proof:
Taking the semilattice axioms in turn:
Theorem: Structure with Commutative Idempotent Associative Operations satisfying Absorption Laws is Lattice

Let $S$ be a set.
Let $\vee$ and $\wedge$ be binary operations which, when applied to $S$, are both:
:closed operations
:commutative operations
:idempotent operations
:associative operations.
Furthermore, let $\vee$ and $\wedge$ satisfy the absorption laws:
:$\forall a, b \in S: a \vee \paren {a \wedge b} = a = a \wedge {a \vee b}$
Then there exists a unique lattice ordering $\preccurlyeq$ on $S$ such that:
:$\forall a, b \in S$:
::$x \vee y = \sup \set {a, b}$
::$x \wedge y = \inf \set {a, b}$
That is:
:$\struct {S, \vee, \wedge, \preccurlyeq}$ is a lattice.

Proof:
We have {{hypothesis}} that:
:$\struct {S, \vee}$ is a commutative idempotent semigroup 
:$\struct {S, \wedge}$ is a commutative idempotent semigroup.
That is, $\struct {S, \vee}$ and $\struct {S, \wedge}$ are semilattices.
We are also given that $\vee$ and $\wedge$ satisfy the absorption laws:
:$\forall a, b \in S: a \vee \paren {a \wedge b} = a = a \wedge {a \vee b}$
Finally we note that from Semilattice has Unique Ordering such that Operation is Supremum, there exists a unique ordering $\preccurlyeq$ on $S$ such that:
:$a \vee b = \sup \set {a, b}$
where $\sup \set {a, b}$ is the supremum of $\set {x, y}$ {{WRT}} $\preccurlyeq$.
Hence, by definition, the ordered structure:
:$\struct {S, \vee, \wedge, \preccurlyeq}$
is a lattice.
{{qed}}
Theorem: Join Operation on Ordered Set such that Every Doubleton admits Supremum is Entropic

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\struct {S, \preccurlyeq}$ be such that every doubleton subset of $S$ admits a supremum.
Let $\vee$ be the join operation on $S$, defined as:
:$\forall a, b \in S: a \vee b = \sup_\preccurlyeq \set {a, b}$
Then $\vee$ is an entropic operation.

Proof:
By definition, $\struct {S, \vee, \preccurlyeq}$ is a join semilattice. 
From Join Semilattice is Semilattice, $\struct {S, \vee, \preccurlyeq}$ is indeed a semilattice.
Then:
{{begin-eqn}}
{{eqn | q = \forall a, b, c, d, \in S
      | l = \paren {a \vee b} \vee \paren {c \vee d}
      | r = a \vee \paren {\paren {b \vee c} \vee d}
      | c = {{Semilattice-axiom|1}}
}}
{{eqn | r = a \vee \paren {\paren {c \vee b} \vee d}
      | c = {{Semilattice-axiom|2}}
}}
{{eqn | r = \paren {a \vee c} \vee \paren {b \vee d}
      | c = {{Semilattice-axiom|1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Closed Elements wrt Closure Operator under Subset Operation is Complete Lattice

Let $S$ be a set.
Let $\cl$ be a closure operator on the power set $\powerset S$ of $S$.
Let $\mathscr C$ be the set of all subsets $T$ of $S$ such that:
:$\map \cl T = T$
Then the algebraic structure $\struct {\mathscr C, \subseteq}$ forms a complete lattice.

Proof:
Recall the closure axioms:
{{:Axiom:Closure Axioms for Power Set}}
First we note that from {{Closure-axiom-powerset|1}} we have that:
:$\map \cl S = S$
and so:
:$S \in \mathscr C$
Let $\AA \subseteq \mathscr C$.
Thus $\AA$ is a set of subsets $T$ of $S$ for all of which $\map \cl T = T$.
From Intersection of Closed Sets is Closed:
:$\ds \cap \AA \in \mathscr C$
The result follows from Set of Subsets which contains Set and Intersection of Subsets is Complete Lattice,
{{qed}}
Theorem: Inverse Relational Structures of Isomorphic Structures are Isomorphic

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let ${\RR_1}^{-1}$ and ${\RR_2}^{-1}$ be the inverses of $\RR_1$ and $\RR_2$ respectively.
Let $f: \struct {S, \RR_1} \to \struct {T, \RR_2}$ be a relation isomorphism.
Then $f: \struct {S, {\RR_1}^{-1} } \to \struct {T, {\RR_2}^{-1} } $ is also a relation isomorphism.

Proof:
{{begin-eqn}}
{{eqn | q =\forall x, y \in S
      | l = x
      | o = {\RR_1}^{-1}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \RR_1
      | r = x
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f y
      | o = \RR_2
      | r = \map f x
      | c = {{Defof|Relation Isomorphism}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f x
      | o = {\RR_2}^{-1}
      | r = \map f y
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Characterisation of Terminal P-adic Expansion/Necessary Condition

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $x \in \Q_p$.
Let the $p$-adic expansion of $x$ terminate.
Then:
:$\exists a \in \N : \exists k \in \Z : x = \dfrac a {p^k}$

Proof:
Let the $p$-adic expansion of $x$ be:
:$x = \ds \sum_{n \mathop = m}^\infty d_n p^n$ 
where:
:$m \in \Z_{\le 0}$
:$\forall n \in \Z_{\ge m}: d_n$ is a $p$-adic digit
:$m < 0 \implies d_m \ne 0$
By the definition of terminates:
:$\exists n_0 \in \N : n_0 \ge m : \forall n \ge n_0 : d_n = 0$
We have:
{{begin-eqn}}
{{eqn | l = x 
      | r = \sum_{n \mathop = m}^{n_0} d_n p^n
      | c = All trailing terms are $0$
}}
{{eqn | r = p^m \paren{\sum_{n \mathop = m}^{n_0} d_n p^{n - m} }
      | c = Extract common $p^m$ factor from each term
}}
{{eqn | r = p^m \paren{\sum_{n \mathop = 0}^{n_0 - m} d_{n + m} p^n }
      | c = Re-indexing the terms
}}
{{end-eqn}}
Let:
:$k = -m$
Let:
:$a = \ds \sum_{n \mathop = 0}^{n_0 - m} d_{n + m} p^n $
Then:
:$x = \dfrac a {p^k}$
The result follows.
Theorem: Characterisation of Terminal P-adic Expansion/Sufficient Condition

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $a \in \N$.
Let $k \in \Z$.
Let $x = \dfrac a {p^k}$.
Then:
:the $p$-adic expansion of $x$ terminates

Proof:
From Basis Representation Theorem, $a$ can be expressed uniquely in the form:
:$\ds a = \sum_{j \mathop = 0}^n d_j p^j$
where:
:$n$ is such that $p^n \le a < p^{n + 1}$
:all the $d_j$ are such that $0 \le d_j < p$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | r = \dfrac a {p^k}
      | c = Hypothesis
}}
{{eqn | r = \dfrac {\ds \sum_{j \mathop = 0}^n d_j p^j} {p^k}
      | c = Replacing $a$ with base $p$ expression
}}
{{eqn | r = \sum_{j \mathop = 0}^n d_j p^{j - k}
      | c = Dividing each term by $p^k$
}}
{{eqn | r = \sum_{i \mathop = -k}^{n-k} d_{i+ k} p^i
      | c = Re-indexing with $i = j - k$
}}
{{end-eqn}}
Let:
:$m = \begin{cases}
-k & : -k \le 0\\
0 & : 0 < -k 
\end{cases}$
For each $i : m \le i \le n-k$, let:
:$e_i = \begin{cases}
d_{i + k} & : -k \le i \le n-k\\
0 & : m \le i < -k
\end{cases}$
For each $i > n-k$, let:
:$e_i = 0$
Then:
:$x = \ds \sum_{i \mathop = m}^\infty e_i p^i$
where:
:$\forall i \ge m: 0 \le e_i < p$
:$\forall i > n-k: e_i = 0$
Hence $\ds \sum_{i \mathop = m}^\infty e_i p^i$ is a terminal $p$-adic expansion by definition.
From P-adic Expansion Representative of P-adic Number is Unique, the $p$-adic expansion of $x$ is:
:$x = \ds \sum_{i \mathop = m}^\infty e_i p^i$
Theorem: Intersection of Antisymmetric Relations is Antisymmetric

The intersection of two antisymmetric relations is also an antisymmetric relation.

Proof:
Let $\RR_1$ and $\RR_2$ be antisymmetric relations on a set $S$.
Let $\RR_3 = \RR_1 \cap \RR_2$.
Hence we have:
{{begin-eqn}}
{{eqn | q = \forall \tuple {x, y} \in \RR_3
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_3
      | c =
}}
{{eqn | q = \forall \tuple {x, y} \in \RR_3
      | l = \tuple {x, y}
      | o = \in
      | r = \RR_1
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = \tuple {x, y}
      | o = \in
      | r = \RR_2
      | c =
}}
{{end-eqn}}
{{AimForCont}} $\RR_3$ is not antisymmetric.
Then:
{{begin-eqn}}
{{eqn | q = \exists x, y \in S: x \ne y, \tuple {x, y} \in \RR_3
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_3
      | c =
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_1
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_2
      | c =
}}
{{end-eqn}}
Hence we have:
{{begin-eqn}}
{{eqn | q = \exists x, y \in S, x \ne y, \tuple {x, y} \in \RR_1
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_1
      | c = 
}}
{{eqn | q = \exists x, y \in S, x \ne y, \tuple {x, y} \in \RR_2
      | l = \tuple {y, x}
      | o = \in
      | r = \RR_2
      | c =
}}
{{end-eqn}}
That is, neither $\RR_1$ nor $\RR_2$ are antisymmetric.
From this contradiction it follows that $\RR_1 \cap \RR_2$ is an antisymmetric relation.
{{qed}}
Category:Antisymmetric Relations
Category:Set Intersection
7tkz2dlf0hlay625ssas0o1qf4mh0s8
Theorem: Intersection of Orderings is Ordering

Let $A$ be a set.
Let $\RR$ and $\SS$ be orderings on $A$.
Then $\RR \cap \SS$ is an ordering on $A$.

Proof:
By definition of ordering:
:$\RR$ and $\SS$ are reflexive
:$\RR$ and $\SS$ are transitive
:$\RR$ and $\SS$ are antisymmetric.
We have:
:Intersection of Reflexive Relations is Reflexive
:Intersection of Transitive Relations is Transitive
:Intersection of Antisymmetric Relations is Antisymmetric
and the result follows.
{{qed}}
Theorem: Inverse of Diagonal Relation

Let $S$ be a set.
Let $\Delta_S$ denote the diagonal relation on $S$.
Let ${\Delta_S}^{-1}$ denote the inverse of $\Delta_S$.
Then:
:${\Delta_S}^{-1} = \Delta_S$

Proof:
By definition of diagonal relation:
:$\Delta_S = \set {\tuple {x, x} \in S \times S: x \in S}$
By definition of inverse relation:
:${\Delta_S}^{-1} = \set {\tuple {x, x} \in S \times S: x \in S}$
Hence it follows that:
:$\tuple {x, x} \in \Delta_S \iff \tuple {x, x} \in {\Delta_S}^{-1}$
{{qed}}
Category:Diagonal Relation
Category:Inverse Relations
54e5d1t1lkk0macwo7d28a34gnggrzq
Theorem: Union of Antisymmetric Relation with Inverse is Antisymmetric iff Diagonal

Let $\RR$ be an antisymmetric relation on a set $S$.
Then:
:$\RR \cup \RR^{-1}$ is antisymmetric
{{iff}}
:$\RR = \Delta_S$
where:
:$\RR^{-1}$ denotes the inverse of $\RR$
:$\Delta_S$ denotes the diagonal relation
:$\cup$ denotes set union.

Proof:
As asserted, let $\RR$ be an antisymmetric relation.
Theorem: Union of Orderings is not necessarily Ordering

Let $A$ be a set.
Let $\RR$ and $\SS$ be orderings on $A$.
Then $\RR \cup \SS$ is not necessarily an ordering on $A$.

Proof:
Let $\RR$ be an ordering as asserted.
Let $\SS$ be the dual ordering of $\RR$.
From Dual Ordering is Ordering, $\SS$ is an ordering.
By definition, the dual of $\RR$ is the inverse of $\RR$:
:$\SS = \RR^{-1}$
From Union of Antisymmetric Relation with Inverse is Antisymmetric iff Diagonal, it is generally not the case that $\RR \cup \RR^{-1}$ is antisymmetric.
Hence, in general, $\RR \cup \RR^{-1}$ is not an ordering.
{{qed}}
Theorem: Composite of Reflexive Relations is Reflexive

Let $A$ be a set.
Let $\RR$ and $\SS$ be reflexive relations on $A$.
Then their composite $\RR \circ \SS$ is also reflexive.

Proof:
Recall the definition of composition of relations:
{{:Definition:Composition of Relations}}
Hence in this particular context:
:$\RR \circ \SS := \set {\tuple {x, z} \in A \times A: \exists y \in A: \tuple {x, y} \in \SS \land \tuple {y, z} \in \RR}$
Let $x \in A$ be arbitrary.
By definition of reflexive relation:
:$\tuple {x, x} \in \SS$
:$\tuple {x, x} \in \RR$
and so setting $y = z = x$:
:$\tuple {x, x} \in \set {\tuple {x, z} \in A \times A: \exists y \in A: \tuple {x, y} \in \SS \land \tuple {y, z} \in \RR}$
Hence the result.
{{qed}}
Category:Composite Relations
Category:Reflexive Relations
7i5rb5eby8tepk92x3qxby9u3n128jk
Theorem: Composite of Symmetric Relations is not necessarily Symmetric

Let $A$ be a set.
Let $\RR$ and $\SS$ be symmetric relations on $A$.
Then their composite $\RR \circ \SS$ is not necessarily symmetric.

Proof:
Proof by Counterexample:
Let:
{{begin-eqn}}
{{eqn | l = A
      | r = \set {1, 2, 3}
}}
{{eqn | l = \RR
      | r = \set {\tuple {1, 2}, \tuple {2, 1} }
}}
{{eqn | l = \SS
      | r = \set {\tuple {2, 3}, \tuple {3, 2} }
}}
{{end-eqn}}
We note that both $\RR$ and $\SS$ are symmetric relations on $A$.
We have by definition of composition of relations that:
:$\RR \circ \SS = \set {\tuple {x, z} \in A \times A: \exists y \in A: \tuple {x, y} \in \SS \land \tuple {y, z} \in \RR}$
By inspection, we see that:
:$\RR \circ \SS = \set {\tuple {3, 1} }$
demonstrating that $\RR \circ \SS$ is not symmetric.
{{qed}}
Category:Composite Relations
Category:Symmetric Relations
i0gsfhnwuvxxdvuvwc4cs220n20m38u