avewright/proofwiki-math huggingface dataset:
Theorem: Supremum is Increasing relative to Product Ordering

Let $\struct {S, \preceq}$ be an ordered set.
Let $I$ be a set.
Let $f, g: I \to S$.
Let $f \sqbrk I$ denote the image of $I$ under $f$.
Let:
:$\forall i \in I: \map f i \preceq \map g i$
That is, let $f \preceq g$ in the product ordering.
Let $f \sqbrk I$ and $g \sqbrk I$ admit suprema.
Then:
:$\sup f \sqbrk I \preceq \sup g \sqbrk I$

Proof:
Let $x \in f \sqbrk I$.
Then:
:$\exists j \in I: \map f j = x$
Then:
:$\map f j \prec \map g j$
By the definition of supremum:
:$\sup g \sqbrk I$ is an upper bound of $g \sqbrk I$
Thus:
:$\map g j \preceq \sup g \sqbrk I$
Since $\preceq$ is transitive:
:$x = \map f j \preceq \sup g \sqbrk I$
Since this holds for all $x \in f \sqbrk I$, $\sup g \sqbrk I$ is an upper bound of $f \sqbrk I$.
Thus by the definition of supremum:
:$\sup f \sqbrk I \preceq \sup g \sqbrk I$
{{qed}}
Category:Order Theory
Category:Increasing Mappings
nvbnmi1wddllqasc5avzmdeqpyss62q
Theorem: Reflexive Closure of Strict Ordering is Ordering

Let $S$ be a set.
Let $\prec$ be a strict ordering on $S$.
Let $\preceq$ be the reflexive closure of $\prec$.
Then $\preceq$ is an ordering.

Proof:
Since $\prec$ is a strict ordering, it is by definition transitive and asymmetric.
By Asymmetric Relation is Antisymmetric, $\prec$ is antisymmetric.
Thus by Reflexive Closure of Transitive Antisymmetric Relation is Ordering, $\preceq$ is an ordering.
{{qed}}
Theorem: Reflexive Closure is Reflexive

Let $\RR$ be a relation on a set $S$.
Then $\RR^=$, the reflexive closure of $\RR$, is reflexive.

Proof:
Recall the definition of reflexive closure:
:$\RR^= := \RR \cup \Delta_S$
From Set is Subset of Union:
:$\Delta_S \subseteq \RR^=$
The result follows directly from Relation Contains Diagonal Relation iff Reflexive.
{{qed}}
Theorem: Equivalence of Definitions of Reflexive Closure

{{TFAE|def = Reflexive Closure}}
Let $\RR$ be a relation on a set $S$.

Proof:
Let $\RR$ be a relation on a set $S$.
Theorem: Reflexive Closure is Inflationary

Let $S$ be a set.
Let $R$ denote the set of all endorelations on $S$.
Then the reflexive closure operator is an inflationary mapping on $R$.

Proof:
Let $\RR \in R$.
The reflexive closure $\RR^=$ of $\RR$ is defined as:
:$\RR^= := \RR \cup \Delta_S$
From Set is Subset of Union:
:$\RR \subseteq \RR^=$
Hence the reflexive closure operator is an inflationary mapping.
Theorem: Reflexive Closure is Order Preserving

Let $S$ be a set.
Let $R$ denote the set of all endorelations on $S$.
Then the reflexive closure operator is an order preserving mapping on $R$.
That is:
:$\forall \RR, \SS \in R: \RR \subseteq \SS \implies \RR^= \subseteq \SS^=$
where $\RR^=$ and $\SS^=$ denote the reflexive closure of $\RR$ and $\SS$ respectively.

Proof:
Let $\RR, \SS \in R$.
Suppose:
:$\RR \subseteq \SS$
Their respective reflexive closures $\RR^=$ and $\SS^=$ are defined as:
:$\RR^= := \RR \cup \Delta_S$
:$\SS^= := \SS \cup \Delta_S$
Hence by {{Corollary|Set Union Preserves Subsets}}:
:$\RR^= \subseteq \SS^=$
Theorem: Reflexive Closure is Idempotent

Let $S$ be a set.
Let $R$ denote the set of all endorelations on $S$.
Then the reflexive closure operator is an idempotent mapping on $R$.
That is:
:$\forall \RR \in R: \RR^= = \paren {\RR^=}^=$
where $\RR^=$ denotes the reflexive closure of $\RR$.

Proof:
Let $\RR \in R$.
By the definition of reflexive closure:
:$\RR^= = \RR \cup \Delta_S$
:$\paren {\RR^=}^= = \paren {\RR \cup \Delta_S} \cup \Delta_S$
By Union is Associative:
:$\paren {\RR^=}^= = \RR \cup \paren {\Delta_S \cup \Delta_S}$
By Set Union is Idempotent:
:$\paren {\RR^=}^= = \RR \cup \Delta_S$
Hence:
:$\forall \RR \in R: \RR^= = \paren {\RR^=}^=$
Theorem: Transitive Closure of Relation Always Exists

Let $\RR$ be a relation on a set $S$.
Then the transitive closure $\RR^+$ of $\RR$ always exists.

Proof:
=== Outline ===
{{:Transitive Closure of Relation Always Exists/Outline}}{{qed|lemma}}
By definition, the trivial relation $\TT = S \times S$ on $S$ contains $\RR$ as a subset.
Further, $\TT$ is transitive by Trivial Relation is Equivalence.
Thus there exists at least one transitive relation on $S$ that contains $\RR$.
Let $\RR^\cap$ be defined as the intersection of all transitive relations on $S$ that contain $\RR$:
:$\ds \RR^\cap := \bigcap \set {\RR': \RR' \text{ is transitive and } \RR \subseteq \RR'}$
By Intersection of Transitive Relations is Transitive, $\RR^\cap$ is also a transitive relation on $S$.
By Set Intersection Preserves Subsets, it also holds that $\RR \subseteq \RR^\cap$.
Lastly, by Intersection is Subset, for any transitive relation $\RR'$ containing $\RR$, it must be that $\RR^\cap \subseteq \RR'$.
Thus $\RR^\cap$ is indeed the minimal transitive relation on $S$ containing $\RR$.
That is, $\RR^+ = \RR^\cap$, and thence the transitive closure of $\RR$ exists.
{{qed}}
Theorem: Equivalence of Definitions of Transitive Closure of Relation/Union of Compositions is Smallest

Let $\RR$ be a relation on a set $S$.
Let:
:$\RR^n := \begin {cases} \RR & : n = 0 \\ \RR^{n - 1} \circ \RR & : n > 0 \end {cases}$
where $\circ$ denotes composition of relations.
{{explain|Really? I would have thought $\RR^1 {{=}} \RR$, not $\RR^0 {{=}} \RR$. If anything, the diagonal relation $\Delta_S$ should be $\RR^0$.}}
Finally, let:
:$\ds \RR^+ = \bigcup_{i \mathop \in \N} \RR^i$
Then $\RR^+$ is the smallest transitive relation on $S$ that contains $\RR$.

Proof:
==== $\RR^+$ is Transitive ====
By Relation contains Composite with Self iff Transitive, we can prove that $\RR^+$ is transitive by proving the following:
:$\RR^+ \circ \RR^+ \subseteq \RR^+$
Let $\tuple {a, c} \in \RR^+ \circ \RR^+$.
Then:
:$\exists b \in S: \tuple {a, b} \in \RR^+, \tuple {b, c} \in \RR^+$
Thus:
:$\exists n \in \N: \tuple {a, b} \in \RR^n$
:$\exists m \in \N: \tuple {b, c} \in \RR^m$
From Composition of Relations is Associative:
:$\RR^{n + m} = \RR^n \circ \RR^m$
so:
:$\tuple {a, c} \in \RR^{n + m} \subseteq \RR^+$
Since this holds for all $\tuple {a, c} \in \RR^+ \circ \RR^+$:
:$\RR^+ \circ \RR^+ \subseteq \RR^+$
Thus $\RR^+$ is transitive.
{{qed|lemma}}
==== $\RR^+$ contains $\RR$ ====
$\RR \subseteq \RR^+$ by Set is Subset of Union of Family.
==== $\RR^+$ is Smallest ====
Let $\RR'$ be a transitive relation on $S$ such that $\RR \subseteq \RR'$.
We must show that $\RR^+ \subseteq \RR'$.
Let $\tuple {a, b} \in \RR^+$.
That is:
:$a \mathrel \RR b$
Then:
:$\exists n \in \N: \tuple {a, b} \in \RR^n$
Thus by the definition of composition of relations, there exists $x_{n - 1} \in S$ such that:
:$a \mathrel {\RR^{n - 1} } x_{n - 1} \land x_{n - 1} \mathrel \RR b$
Likewise there exists $x_{n - 2} \in S$ such that:
:$a \mathrel {\RR^{n - 2} } x_{n - 2} \land x_{n - 2} \mathrel \RR x_{n - 1}$
And so forth there exist elements $x_0, \dots, x_n \in S$ such that:
:$x_0 = a$
:$x_n = b$
:$\forall k \in \N_n: x_k \mathrel \RR x_{k + 1}$
Since $\RR \subseteq \RR'$:
:$\forall k \in \N_n: x_k \mathrel {\RR'} x_{k + 1}$
Since $\RR'$ is transitive:
:$a \mathrel {\RR'} b$
That is:
:$\tuple {a, b} \in \RR'$
Since this holds for all $\tuple {a, b} \in \RR^+$:
:$\RR^+ \subseteq \RR'$
Since this holds for all transitive relations $\RR'$ that contain $\RR$:
:$\RR^+$ is the smallest transitive relation containing $\RR$.
{{qed}}
Theorem: Equivalence of Definitions of Transitive Closure of Relation/Finite Chain Equivalent to Union of Compositions

The finite chain and union of compositions definitions of '''transitive closure''' are equivalent.

Proof:
{{explain|more detail required}}
Follows from the definition of composition of relations.
{{qed}}
Theorem: Chasles' Relation

Let $\EE$ be an affine space.
Let $p, q, r \in \EE$ be points.
Then:
:$\vec {p q} = \vec {p r} + \vec {r q}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \vec {p r} + \vec {r q}
      | r = \paren {r - p} + \paren {q - r}
      | c = {{Defof|Vector (Affine Geometry)|Vector in Affine Space}}
}}
{{eqn | r = \paren {r + \paren {q - r} } - p
      | c = {{Defof|Affine Space}}: axiom $(\text A 3)$
}}
{{eqn | r = q - p
      | c = {{Defof|Affine Space}}: axiom $(\text A 1)$
}}
{{eqn | r = \vec{p q}
      | c = {{Defof|Vector (Affine Geometry)|Vector in Affine Space}}
}}
{{end-eqn}}
{{Qed}}
{{Namedfor|Michel Chasles|cat = Chasles}}
Category:Affine Geometry
bx95rwdeunrmmg14ssgt4opynmv5wjz
Theorem: Affine Coordinates are Well-Defined

Let $\EE$ be an affine space with difference space $V$ over a field $k$.
Let $\RR = \left({p_0, e_1, \ldots, e_n}\right)$ be an affine frame in $\EE$.
Define a mapping $\Theta_\RR : k^n \to \EE$ by:
:$\ds \map {\Theta_\RR} {\lambda_1, \ldots, \lambda_n} = p_0 + \sum_{i \mathop = 1}^n \lambda_i e_i$
Then $\Theta_\RR$ is a bijection.

Proof:
=== Proof of Surjection ===
Let $p \in \EE$.
Let $v = p - p_0 \in V$.
Let $\tuple {\lambda_1, \ldots, \lambda_n}$ be coordinates of $v$ in the basis $\tuple {e_1, \ldots, e_n}$.
Then:
{{begin-eqn}}
{{eqn | l = p_0 + \sum_{i \mathop = 1}^n \lambda_ie_i
      | r = p_0 + v
}}
{{eqn | r = p_0 + \paren {p - p_0}
}}
{{eqn | r = p
}}
{{end-eqn}}
thus demonstrating that $\Theta_\RR$ is a surjection.
Theorem: Barycenter Exists and is Well Defined

Let $\EE$ be an affine space over a field $k$.
Let $p_1, \ldots, p_n \in \EE$ be points.
Let $\lambda_1, \ldots, \lambda_n \in k$ such that $\ds \sum_{i \mathop = 1}^n \lambda_i = 1$.
Then the barycentre of $p_1, \ldots, p_n$ with weights $\lambda_1, \ldots, \lambda_n$ exists and is unique.

Proof:
Let $r$ be any point in $\EE$.
Set:
:$\ds q = r + \sum_{i \mathop = 1}^n \lambda_i \vec{r p_i}$
We are required to prove that for any other point $m \in \EE$:
:$\ds q = m + \sum_{i \mathop = 1}^n \lambda_i \vec{m p_i}$
So:
{{begin-eqn}}
{{eqn | l = m + \sum_{i \mathop = 1}^n \lambda_i \vec{m p_i}
      | r = m + \sum_{i \mathop = 1}^n \lambda_i \paren {\vec{m r} + \vec{r p_i} }
      | c = Chasles' Relation
}}
{{eqn | r = m + \paren {\sum_{i \mathop = 1}^n \lambda_i} \vec {m r} + \sum_{i \mathop = 1}^n \lambda_i \vec {r p_i}
}}
{{eqn | r = m + \vec {m r} + \sum_{i \mathop = 1}^n \lambda_i \vec{r p_i}
      | c = by the assumption $\ds \sum_{i \mathop = 1}^n \lambda_i = 1$
}}
{{eqn | r = r + \sum_{i \mathop = 1}^n \lambda_i \vec{r p_i}
      | c = Axiom $(1)$ for an affine space
}}
{{eqn | r = q
      | c = Definition of $q$
}}
{{end-eqn}}
Hence the result.
{{Qed}}
Category:Affine Geometry
2r45dl2dqjz7w74obom4qpycziw8m34
Theorem: Transitive Chaining

Let $\RR$ be a transitive relation on a set $S$.
Let $n \in \N$ be a natural number.
Let $n \ge 2$.
Let $\sequence {x_k}_{k \mathop \in \set {1, 2, \dots, n} }$ be a sequence of $n$ terms.
For each $k \in \set {1, 2, \dots, n - 1}$, let $x_k \mathrel \RR x_{k + 1}$.
That is, let $x_1 \mathrel \RR x_2$, $x_2 \mathrel \RR x_3, \dotsc, x_n - 1 \mathrel \RR x_n$.
Then:
:$x_1 \mathrel \RR x_n$

Proof:
The proof proceeds by induction on $n$, the number of terms in the sequence.
We first define a propositional function, $P$, as follows:
For each $n \in \N$ such that $n \ge 2$, let $\map P n$ be the proposition that if both of the following hold:
:$\sequence {x_k}_{k \mathop \in \set {1, 2, \dots, n} }$ is a sequence of $n$ terms
:$\forall k \in \set {1, 2, \dots, n - 1}: x_k \mathrel \RR x_{k + 1}$
then:
:$x_1 \mathrel \RR x_n$
Theorem: Szpilrajn Extension Theorem

Let $\struct {S, \prec}$ be a strictly ordered set.
{{Disambiguate|Definition:Strictly Ordered Set}}
Then there is a strict total ordering on $S$ of which $\prec$ is a subset.

Proof:
{{proof wanted}}
{{Namedfor|Edward Szpilrajn|cat = Marczewski}}
Category:Order Theory
lji5i6b8gp30a7jge1hz1i76m5xmudk
Theorem: Characterization of Interior of Triangle

Let $\triangle$ be a triangle embedded in $\R^2$.
Denote the vertices of $\triangle$ as $A_1, A_2, A_3$.
For $i \in \set {1, 2, 3}$, put $j = i \bmod 3 + 1$, $k = \paren {i + 1} \bmod 3 + 1$, and:
:$U_i = \set {A_i + s t \paren {A_j - A_i} + \paren {1 - s} t \paren {A_k - A_i} : s \in \openint 0 1, t \in \R_{>0} }$
Then:
:$\ds \Int \triangle = \bigcap_{i \mathop = 1}^3 U_i$
where $\Int \triangle$ denotes the interior of the boundary of $\triangle$.

Proof:
From Boundary of Polygon is Jordan Curve, it follows that the boundary of $\triangle$ is equal to the image of a Jordan curve, so $\Int \triangle$ is well-defined.
Theorem: Equivalence of Definitions of Reflexive Transitive Closure

Let $\RR$ be a relation on a set $S$.
{{TFAE|def = Reflexive Transitive Closure}}

Proof:
The result follows from:
:Transitive Closure of Reflexive Relation is Reflexive
:Reflexive Closure of Transitive Relation is Transitive
:Composition of Compatible Closure Operators
{{qed}}
Category:Reflexive Closures
Category:Transitive Closures
3zuw09718neju3nn5iksghyv70vs1p2
Theorem: Intersection of Relation with Inverse is Symmetric Relation

Let $\RR$ be a relation on a set $S$.
Then $\RR \cap \RR^{-1}$, the intersection of $\RR$ with its inverse, is symmetric.

Proof:
Let $\tuple {x, y} \in \RR \cap \RR^{-1}$
By definition of intersection:
:$\tuple {x, y} \in \RR$
:$\tuple {x, y} \in \RR^{-1}$
By definition of inverse relation:
:$\tuple {x, y} \in \RR \implies \tuple {y, x} \in \RR^{-1}$
:$\tuple {x, y} \in \RR^{-1} \implies \tuple {y, x} \in \paren {\RR^{-1} }^{-1}$
By Inverse of Inverse Relation the second statement may be rewritten:
:$\tuple {x, y} \in \RR \implies \tuple {y, x} \in \RR^{-1}$
:$\tuple {x, y} \in \RR^{-1} \implies \tuple {y, x} \in \RR$
Then by definition of intersection:
:$\tuple {y, x} \in \RR \cap \RR^{-1}$
Hence $\RR \cap \RR^{-1}$ is symmetric.
{{qed}}
Theorem: Intersection of Closed Sets is Closed/Closure Operator

Let $S$ be a set.
Let $f: \powerset S \to \powerset S$ be a closure operator on $S$.
Let $\CC$ be the set of all subsets of $S$ that are closed with respect to $f$.
Let $\AA \subseteq \CC$.
Then $\bigcap \AA \in \CC$.

Proof:
Let $Q = \bigcap \AA$.
By the definition of closure operator, $f$ is inflationary, order-preserving, and idempotent.
Let $A \in \AA$.
By Intersection is Largest Subset, $Q \subseteq A$.
Since $f$ is order-preserving, $\map f Q \subseteq \map f A$.
By the definition of closed set, $\map f A = A$
Thus $\map f Q \subseteq A$.
This holds for all $A \in \AA$.
Thus by Intersection is Largest Subset:
:$\map f Q \subseteq \bigcap \AA$
Since $\bigcap \AA = Q$:
:$\map f Q \subseteq Q$
Since $f$ is inflationary:
:$Q \subseteq \map f Q$
Thus by definition of set equality:
:$Q = \map f Q$
Therefore $Q$ is closed with respect to $f$.
{{qed}}
Category:Closure Operators
Category:Set Intersection
0wx60nxfhxnwbqfzj1mo6nccgfu2jok
Theorem: Closure is Closed/Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $\cl: \powerset S \to \powerset S$ be a closure operator.
Let $T \subseteq S$.
Then $\map \cl T$ is a closed set with respect to $\cl$.

Proof:
By the definition of closure operator, $\cl$ is idempotent.
Therefore $\map \cl {\map \cl T} = \map \cl T$, so $\map \cl T$ is closed.
{{qed}}
Category:Closure Operators
84pspzef6qd7pt11nc0mnk94pg71ies
Theorem: Relation Intersection Inverse is Greatest Symmetric Subset of Relation

Let $\RR$ be a relation on a set $S$.
Let $\powerset \RR$ be the power set of $\RR$.
By definition, $\powerset \RR$ is the set of all relations on $S$ that are subsets of $\RR$.
Then the greatest element of $\powerset \RR$ that is symmetric is:
:$\RR \cap \RR^{-1}$

Proof:
By Intersection of Relation with Inverse is Symmetric Relation:
:$\RR \cap \RR^{-1}$ is a symmetric relation.
Suppose for some $\SS \in \powerset \RR$ that $S$ is symmetric and not equal to $\RR \cap \RR^{-1}$.
We will show that it is a proper subset of $\RR \cap \RR^{-1}$.
Suppose $\tuple {x, y} \in \SS$.
Then as $\SS \subseteq \RR$:
:$\tuple {x, y} \in \RR$
As $\SS$ is symmetric:
:$\tuple {x, y} \in \SS$
So as $\SS \subseteq \RR$:
:$\tuple {x, y} \in \RR$
By definition of inverse relation:
:$\tuple {x, y} \in \RR^{-1}$
By definition of intersection:
:$\tuple {x, y} \in \RR \cap \RR^{-1}$
Thus:
:$\tuple {x, y} \in \SS \implies \tuple {x, y} \in \RR \cap \RR^{-1}$
By definition of subset:
:$\SS \subseteq \RR \cap \RR^{-1}$
Finally, as we assumed $\SS \ne \RR \cap \RR^{-1}$:
:$\SS \subset \RR \cap \RR^{-1}$
Hence the result.
{{qed}}
Category:Relation Theory
Category:Symmetric Relations
6k95y20lcui80oc5hcca1henqlhj01p
Theorem: Composition of Compatible Closure Operators

Let $S$ be a set.
Let $f, g: \powerset S \to \powerset S$ be closure operators on $S$.
Let $\CC_f$ and $\CC_g$ be the sets of closed sets of $S$ with respect to $f$ and $g$ respectively.
For each subset $T$ of $S$, let the following hold:
:$(1): \quad$ If $T$ is closed with respect to $g$, then $\map f T$ is closed with respect to $g$.
::That is, if $T \in \CC_g$ then $\map f T \in \CC_g$.
:$(2): \quad$ If $T$ is closed with respect to $f$, then $\map g T$ is closed with respect to $f$.
::That is, if $T \in \CC_f$ then $\map g T \in \CC_f$.
Let $\CC_h = \CC_f \cap \CC_g$.
Then:
:$\CC_h$ induces a closure operator $h$ on $S$
:$f \circ g = g \circ f = h$, where $\circ$ represents composition of mappings.

Proof:
First we show that $\CC_h$ induces a closure operator on $S$.
Let $\AA \subseteq \CC_h$.
By Intersection is Largest Subset:
:$\AA \subseteq \CC_f$
and:
:$\AA \subseteq \CC_g$
Thus by Intersection of Closed Sets is Closed/Closure Operator:
:$\ds \bigcap \AA \in \CC_f$
and
:$\ds \bigcap \AA \in \CC_g$
Thus by the definition of set intersection:
:$\ds \bigcap \AA \in \CC_h$
Thus by Closure Operator from Closed Sets, $C_h$ induces a closure operator $h$ on $S$.
Now we will show that $f \circ g = h$.
Having established that, it can be seen that $g \circ f = h$ will hold by reversing the variable names.
Let $T \subseteq S$.
By definition of closed set:
:$\map f {\map g T} \in \CC_f$
:$\map g T \in \CC_g$
By the premise:
:$\map f {\map g T} \in \CC_g$
Thus by definition of set intersection:
:$\map f {\map g T} \in \CC_f \cap \CC_g = C_h$
So $\map f {\map g T}$ is closed with respect to $h$.
By Set Closure is Smallest Closed Set/Closure Operator:
:$\map h T \subseteq f {\map g T}$
By definition of closed set:
:$\map h T \in C_h$
Thus by definition of set intersection:
:$\map h T \in C_f$
and
:$\map h T \in C_g$
By Set Closure is Smallest Closed Set/Closure Operator:
:$\map g T \subseteq \map h T$
By Closure Operator: Axiom $(2)$ $f$ is order-preserving:
:$\map f {\map g T} \subseteq \map f {\map h T}$
Recall that $\map h T \in C_f$.
By definition of closed set:
:$\map f {\map h T} = \map h T$
Thus:
:$\map f {\map g T} \subseteq \map h T$
We have that:
:$\map h T \subseteq \map f {\map g T}$
So by definition of set equality:
:$\map h T = \map f {\map g T}$
{{qed}}
Category:Closure Operators
s9ppvpojp6tnne6rjsigko3xqykbc8l
Theorem: Closure is Closed

Let $\struct {S, \preceq}$ be an ordered set.
Let $\cl: S \to S$ be a closure operator.
Let $x \in S$.
Then $\map \cl x$ is a closed element of $S$ with respect to $\cl$.

Proof:
By the definition of closure operator, $\cl$ is idempotent.
Therefore:
:$\map \cl {\map \cl x} = \map \cl x$
It follows by definition that $\map \cl x$ is a closed element.
{{qed}}
Theorem: Closure Operator from Closed Elements

Let $\struct {S, \preceq}$ be an ordered set.
Let $C \subseteq S$.
Suppose that $C$ is a subset of $S$ with the property that every element of $S$ has a smallest successor in $C$.
Let $\cl: S \to S$ be defined as follows:
For $x \in S$:
:$\map \cl x = \map \min {C \cap x^\succeq}$
where $x^\succeq$ is the upper closure of $x$.
That is, let $\map \cl x$ be the smallest successor of $x$ in $C$.
Then:
:$\cl$ is a closure operator on $S$
:The closed elements of $\cl$ are precisely the elements of $C$.

Proof:
=== Inflationary ===
$x$ is a lower bound of $x^\succeq$.
Hence by Lower Bound for Subset, $x$ is also a lower bound of $C \cap x^\succeq$.
By the definition of smallest element, $x \preceq \map \cl x$.
{{qed|lemma}}
Theorem: Product of Affine Spaces is Affine Space

Let $\EE, \FF$ be affine spaces.
Let $\GG = \EE \times \FF$ be the product of $\EE$ and $\FF$.
Then $\GG$ is an affine space.

Proof:
Let $G = \vec \GG$ be the difference space of $\GG$.
We are required to show that the following axioms are satisfied:
{{begin-axiom}}
{{axiom | n = 1
        | q = \forall p, q \in \GG
        | m = p + \paren {q - p} = q
}}
{{axiom | n = 2
        | q = \forall p \in \GG: \forall u, v \in G
        | m = \paren {p + u} + v = p + \paren {u + v}
}}
{{axiom | n = 3
        | q = \forall p, q \in \GG: \forall u \in G
        | m = \paren {p - q} + u = \paren {p + u} - q
}}
{{end-axiom}}
Proof of $(1)$:
Let $p = \tuple {p', p' '}, q = \tuple {q', q' '} \in \GG$.
We have:
{{begin-eqn}}
{{eqn | l = p + \paren {q - p}
      | r = \tuple {p', p' '} + \paren {\tuple {q', q' '} - \tuple {p', p' '} }
}}
{{eqn | r = \tuple {p', p' '} + \tuple {q' - p', q' ' - p' '}
      | c = Definition of $-$ in Product Space
}}
{{eqn | r = \tuple {p' + \paren {q' - p'}, p' ' + \paren {q' ' - p' '} }
      | c = Definition of $+$ in Product Space
}}
{{eqn | r = \tuple {q' , q' '}
      | c = Axiom $(1)$ in Affine Spaces $\EE$, $\FF$
}}
{{end-eqn}}
{{qed|lemma}}
Proof of $(2)$:
Let $p = \tuple {p', p' '} \in \GG$.
Let $u = \tuple {u', u' '}, v = \tuple {v', v' '} \in G$.
We have:
{{begin-eqn}}
{{eqn | l = \paren {p + u} + v
      | r = \paren {\tuple {p', p' '} + \tuple {u', u' '} } + \tuple {v', v' '}
}}
{{eqn | r = \tuple {p' + u', p' ' + u' '} + \tuple {v', v' '}
      | c = Definition of $+$ in Product Space
}}
{{eqn | r = \tuple {\paren {p' + u'} + v', \paren {p' ' + u' '} + v' '}
      | c = Definition of $+$ in Product Space
}}
{{eqn | r = \tuple {p' + \paren {u' + v'}, p' ' + \paren {u' ' + v' '} }
      | c = Axiom $(2)$ in Affine Spaces $\EE$, $\FF$
}}
{{eqn | r = \tuple {p', p' '} + \paren {\tuple {u', u' '} + \tuple {v', v' '} }
      | c = Definition of $+$ in Product Space
}}
{{eqn | r = p + \paren {u + v}
}}
{{end-eqn}}
{{qed|lemma}}
Proof of $(3)$:
Let $p = \tuple {p', p' '}, q = \tuple {q', q' '} \in \GG$.
Let $u = \tuple {u', u' '} \in G$.
We have:
{{begin-eqn}}
{{eqn | l = \paren {p - q} + u
      | r = \paren {\tuple {p', p' '} - \tuple {q', q' '} } + \tuple {u', u' '}
}}
{{eqn | r = \tuple {\paren {p' - q'} + u', \paren {p' ' - q' '} + u' '}
      | c = Definition of $+,-$ in Product Space
}}
{{eqn | r = \tuple {\paren {p' + u'} - q', \paren {p' ' + u' '} - q' '}
      | c = Axiom $(3)$ in Affine Spaces $\EE$, $\FF$
}}
{{eqn | r = \paren {\tuple {p', p' '} + \tuple {u', u' '} } - \tuple {q', q' '}
      | c = Definition of $+,-$ in Product Space
}}
{{eqn | r = \paren {p - q} + u
}}
{{end-eqn}}
{{Qed}}
Category:Affine Geometry
spmatxl6rhli7nhzo79anvmmcbqu8d7
Theorem: Intersection of Complete Meet Subsemilattices induces Closure Operator

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $I$ be an indexing set.
Let $\family {f_i}_{i \mathop \in I}$ be an indexed family of closure operators on $S$.
Let $C_i = \map {f_i} S$ be the set of closed elements with respect to $f_i$ for each $i \in I$.
Suppose that for each $i \in I$, $C_i$ is a '''complete meet subsemilattice''' of $S$ in the following sense:
:For each $D \subseteq C_i$, $D$ has an infimum in $S$ such that $\inf D \in C_i$.
Then $C = \ds \bigcap_{i \mathop \in I} C_i$ induces a closure operator on $S$.

Proof:
=== Lemma ===
{{:Intersection of Complete Meet Subsemilattices induces Closure Operator/Lemma}}{{qed|lemma}}
By the lemma, $C$ is a '''complete meet semilattice'''.
Let $x \in S$.
Then $C \cap x^\succcurlyeq$ has an infimum in $S$ which lies in $C$, where $x^\succcurlyeq$ is the upper closure of $x$.
By the definition of infimum:
:$x \preceq \inf \struct {C \cap x^\succcurlyeq}$
so this infimum is in fact the smallest element of $C \cap x^\succcurlyeq$.
Thus $C$ induces a closure operator on $S$ by Closure Operator from Closed Elements.
{{qed}}
Category:Closure Operators
Category:Intersection of Complete Meet Subsemilattices induces Closure Operator
5nepi4jlk89ymt4vqya31f7pqmg9nse