avewright/proofwiki-math huggingface dataset:
Theorem: Lower Section with no Maximal Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $L \subseteq S$.
Then:
:$L$ is a lower section in $S$ with no maximal element
{{iff}}:
:$\ds L = \bigcup \set {l^\prec: l \in L}$
where $l^\prec$ is the strict lower closure of $l$.

Proof:
By Dual Pairs (Order Theory):
* Lower section is dual to upper section.
* Maximal element is dual to minimal element.
* Strict lower closure is dual to strict upper closure.
Thus the theorem holds by the duality principle applied to Upper Section with no Minimal Element.
{{qed}}
Theorem: Lower Section with no Greatest Element is Open in GO-Space

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space.
Let $L$ be a lower section in $S$ with no greatest element.
Then $L$ is open in $\struct {S, \preceq, \tau}$.

Proof:
By Maximal Element in Toset is Unique and Greatest, $L$ has no maximal element.
By Lower Section with no Maximal Element:
:$\ds L = \bigcup \set {l^\prec: l \in L}$
where $l^\prec$ is the strict lower closure of $l$.
By Open Ray is Open in GO-Space and the fact that a union of open sets is open, $L$ is open.
{{qed}}
Theorem: Lower Section is Dual to Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
The following are dual statements:
:$T$ is a lower section in $S$
:$T$ is an upper section in $S$

Proof:
By definition, $T$ is a lower section in $S$ {{iff}}:
:$\forall t \in T: \forall s \in S: s \preceq t \implies s \in T$
The dual of this statement is:
:$\forall t \in T: \forall s \in S: t \preceq s \implies s \in T$
by Dual Pairs (Order Theory).
By definition, this means $T$ is an upper section in $S$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Order Topology equals Dual Order Topology

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\tau$ be the $\preceq$-order topology on $S$.
Let $\tau'$ be the $\succeq$-order topology on $S$, where $\succeq$ is the dual ordering of $\preceq$.
Then $\tau' = \tau$.

Proof:
{{improve|recast in terms of dual statements}}
Let $U$ be an open ray in $\struct {S, \preceq}$.
By Open Ray is Dual to Open Ray, $U$ is an open ray in $\struct {S, \preceq}$.
Since the open rays in a totally ordered set form a sub-basis for the topology on that set, $\tau'$ is finer than $\tau$.
{{explain|Invoke some other duality principle?}}
By the same argument, $\tau$ is finer than $\tau'$.
Thus by definition of set equality:
:$\tau' = \tau$
{{qed}}
Category:Order Topologies
snrnov2i5twblobb64p28gvo8xgjw6c
Theorem: Open Ray is Dual to Open Ray

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $R$ be an open ray in $\struct {S, \preceq}$.
Then $R$ is an open ray in $\struct {S, \succeq}$, where $\succeq$ is the dual ordering of $\preceq$.

Proof:
By the definition of open ray, there is some $p \in S$ such that:
:$R$ is the strict upper or strict lower closure of $p$ with respect to $\preceq$.
By Strict Lower Closure is Dual to Strict Upper Closure, the dual statement is:
:$R$ is the strict upper or strict lower closure of $p$ with respect to $\succeq$.
Thus $R$ is an open ray in $\struct {S, \succeq}$.
{{qed}}
Category:Total Orderings
gy73gxc6wih3diuf1flzimkznoqeau1
Theorem: Topologies on Set form Complete Lattice

Let $X$ be a non-empty set.
Let $\LL$ be the set of topologies on $X$.
Then $\struct {\LL, \subseteq}$ is a complete lattice.

Proof:
Let $\KK \subseteq \LL$.
Then by Intersection of Topologies is Topology:
:$\bigcap \KK \in \LL$
By Intersection is Largest Subset, $\bigcap \LL$ is the infimum of $\KK$.
{{explain}}
Let $\tau$ be the topology generated by the sub-basis $\bigcup \KK$.
Then $\tau \in \LL$ and $\tau$ is the supremum of $\KK$.
We have that each subset of $\LL$ has a supremum and an infimum in $\LL$.
Thus it follows that $\struct {\LL, \subseteq}$ is a complete lattice.
{{qed}}
Category:Topology
Category:Complete Lattices
h9qegsufvqjwyscwz9izjwvhri1cvy9
Theorem: Complement of Lower Section is Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $L$ be a lower section.
Then $S \setminus L$ is an upper section.

Proof:
Let $u \in S \setminus L$.
Let $s \in S$ such that $u \preceq s$.
{{AimForCont}} $s \notin S \setminus L$.
Then $s \in L$.
By definition of lower section, $u \in L$, a contradiction.
Hence $s \in S \setminus L$.
Since this holds for all such $u$ and $s$, $S \setminus L$ is an upper section.
{{qed}}
Theorem: GO-Space Embeds as Closed Subspace of Linearly Ordered Space

Let $\struct {X, \preceq_X, \tau_X}$ be a generalized ordered space.
Then there is a linearly ordered space $\struct {Y, \preceq_Y, \tau_Y}$ and a mapping $\phi: X \to Y$ such that $\phi$ is a topological embedding and an order embedding, and $\phi \sqbrk {X}$ is closed in $Y$.

Proof:
By GO-Space Embeds Densely into Linearly Ordered Space, there is a linearly ordered space $\struct {W, \preceq_W, \tau_W}$ and a mapping $\psi:X \to W$ which is an order embedding and a topological embedding.
{{WLOG}}, assume $X$ is a subspace of $W$.
Let $Y = \set {\tuple {x, 0}: x \in X} \cup \paren {W \setminus X} \times \Z$.
Let $\preceq_Y$ be the restriction to $Y$ of the lexicographic ordering on $W \times \Z$.
Let $\tau_Y$ be the $\preceq_Y$-order topology on $Y$.
Let $\phi: X \to Y$ be given by $\map \phi x = \tuple {x, 0}$.
$\phi$ is clearly an order embedding.
Next, we show that it is a topological embedding:
If $$
Finally, we show that $\phi \sqbrk {X}$ is closed in $Y$:
{{finish}}
Category:Generalized Ordered Spaces
Category:Linearly Ordered Spaces
334fxui71gjwz5xv0sljkslzqi0a7zk
Theorem: Union of Total Ordering with Lower Sections is Total Ordering

Let $\struct {Y, \preceq}$ be a totally ordered set.
Let $X$ be the disjoint union of $Y$ with the set of lower sections of $Y$.
Define a relation $\preceq'$ on $X$ extending $\preceq$ by letting:
:$y_1 \preceq' y_2 \iff y_1 \preceq y_2$
:$y \preceq' L \iff y \in L$
:$L_1 \preceq' L_2 \iff L_1 \subseteq L_2$
:$L \preceq' y \iff y \in Y \setminus L$
Then $\preceq'$ is a total ordering.

Proof:
First note that by Lower Sections in Totally Ordered Set form Chain:
:$\subseteq$ is a total ordering on the set of lower sections.
Also note that by Complement of Lower Section is Upper Section, the complement of each $\preceq$-lower section is a $\preceq$-upper section.
Theorem: Lower Closure is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a subset of $S$.
Let $L$ be the lower closure of $T$.
Then $L$ is a lower section.

Proof:
Let $a \in L$.
Let $b \in S$ with $b \preceq a$.
By the definition of lower closure, there is a $t \in T$ such that $a \preceq t$.
By transitivity, $b \preceq t$.
Thus, again by the definition of lower closure, $b \in L$.
Since this holds for all such $a$ and $b$, $L$ is a lower section.
{{qed}}
Theorem: Lower Closure is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a subset of $S$.
Let $L$ be the lower closure of $T$.
Then $L$ is a lower section.

Proof:
Let $l \in p^\prec$.
Let $s \in S$ with $s \preceq l$.
Then by the definition of strict lower closure:
:$l \prec p$
Thus by Extended Transitivity:
:$s \prec p$
So by the definition of strict lower closure:
:$s \in p^\prec$
Since this holds for all such $l$ and $s$, $p^\prec$ is a lower section.
{{qed}}
Theorem: Lower Closure is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a subset of $S$.
Let $L$ be the lower closure of $T$.
Then $L$ is a lower section.

Proof:
By Dual Pairs (Order Theory):
:strict upper closure is dual to strict lower closure
:Upper section is dual to lower section
Thus the theorem holds by Strict Upper Closure is Upper Section and the duality principle.
{{qed}}
Theorem: Ordered Set is Upper Section in Itself

Let $\struct {S, \preceq}$ be an ordered set.
Then $S$ is an upper section in $S$.

Proof:
Follows immediately from the definition of upper section.
{{qed}}
Category:Upper Sections
fpxlqpe10b7pn56mo2o69xcv5qw295c
Theorem: Ordered Set is Lower Section in Itself

Let $\struct {S, \preceq}$ be an ordered set.
Then $S$ is a lower section in $S$.

Proof:
Follows immediately from the definition of lower section.
{{qed}}
Category:Lower Sections
1t4xb95cwrx8blpmzfytmwfhz8wfd74
Theorem: Ordered Set is Order-Convex in Itself

Let $\struct {S, \preceq}$ be an ordered set.
Then $S$ is an order-convex set in $S$.

Proof:
Follows immediately from the definition of order-convex set.
{{qed}}
Category:Order-Convex Sets
Category:Order Theory
oimlxnt4fz28anw171f4x7tqdk3o8z0
Theorem: Equivalence of Definitions of Generalized Ordered Space/Definition 3 implies Definition 1

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 3:
{{:Definition:Generalized Ordered Space/Definition 3}}
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 1:
{{:Definition:Generalized Ordered Space/Definition 1}}

Proof:
Let $\SS$ be a sub-basis for $\tau$ consisting of upper sections and lower sections.
Let $\BB$ be the set of intersections of finite subsets of $\SS$.
By Upper Section is Order-Convex, Lower Section is Order-Convex and Intersection of Order-Convex Sets is Order-Convex:
:the elements of $\BB$ are order-convex.
From Synthetic Basis formed from Synthetic Sub-Basis, $\BB$ is a basis for $\tau$.
Therefore $\tau$ has a basis consisting of order-convex sets.
Theorem: Strict Upper Closure is Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $p \in S$.
Let $p^\succ$ denote the strict upper closure of $p$.
Then $p^\succ$ is an upper section.

Proof:
Let $u \in p^\succ$.
Let $s \in S$ with $u \preceq s$.
Then by the definition of strict upper closure:
:$p \prec u$
Thus by Extended Transitivity:
:$p \prec s$
So by the definition of strict upper closure:
:$s \in p^\succ$
Since this holds for all such $u$ and $s$, $p^\succ$ is an upper section.
{{qed}}
Theorem: Strict Lower Closure is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $p \in S$.
Let $p^\prec$ denote the strict lower closure of $p$.
Then $p^\prec$ is a lower section.

Proof:
Let $l \in p^\prec$.
Let $s \in S$ with $s \preceq l$.
Then by the definition of strict lower closure:
:$l \prec p$
Thus by Extended Transitivity:
:$s \prec p$
So by the definition of strict lower closure:
:$s \in p^\prec$
Since this holds for all such $l$ and $s$, $p^\prec$ is a lower section.
{{qed}}
Theorem: Strict Lower Closure is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $p \in S$.
Let $p^\prec$ denote the strict lower closure of $p$.
Then $p^\prec$ is a lower section.

Proof:
By Dual Pairs (Order Theory):
:strict upper closure is dual to strict lower closure
:Upper section is dual to lower section
Thus the theorem holds by Strict Upper Closure is Upper Section and the duality principle.
{{qed}}
Theorem: Topology is Discrete iff All Singletons are Open

Let $\struct {S, \tau}$ be a topological space.
Then:
:$\tau$ is the discrete topology on $S$
{{iff}}:
:$\forall x \in S: \set x \in \tau$
That is, {{iff}} every singleton of $S$ is $\tau$-open.

Proof:
=== Sufficient Condition ===
Let $\tau$ be the discrete topology on $S$.
Let $x \in S$ be arbitrary.
Then from Set in Discrete Topology is Clopen it follows directly that $\set x$ is open in $\struct {S, \tau}$.
{{qed|lemma}}
Theorem: Characteristic Function of Universe

Let $S$ be a set.
Let $\chi_S: S \to \set {0, 1}$ be its characteristic function (in itself).
Then:
:$\chi_S = f_1$
where $f_1: S \to \set {0, 1}$ is the constant mapping with value $1$.

Proof:
From Characteristic Function Determined by 1-Fiber, $\chi_S$ is the mapping determined by:
:$\forall s \in S: \map {\chi_S} s = 1 \iff s \in S$
Thus:
:$\forall s \in S: \map {\chi_S} s = 1$
By definition of constant mapping:
:$\chi_S = f_1$
{{qed}}
Category:Characteristic Functions
1wa2giegor01nb3o0133fgh93fanx4u
Theorem: Supremum of Lower Closure of Set

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $T \subseteq S$.
Let $L = T^\preceq$ be the lower closure of $T$ in $S$.
Let $s \in S$
Then $s$ is the supremum of $T$ {{iff}} it is the supremum of $L$.

Proof:
By Supremum and Infimum are Unique we need only show that $s$ is a supremum of $L$ {{iff}} it is a supremum of $T$.
Theorem: Upper Closure is Smallest Containing Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $U = T^\succeq$ be the upper closure of $T$.
Then $U$ is the smallest upper section containing $T$ as a subset.

Proof:
Follows from Upper Closure is Closure Operator and Set Closure is Smallest Closed Set/Closure Operator.
{{qed}}
Theorem: Upper Closure is Closure Operator

Let $\struct {S, \preceq}$ be an ordered set.
Let $T^\succeq$ be the upper closure of $T$ for each $T \subseteq S$.
Then $\cdot^\succeq$ is a closure operator.

Proof:
=== Inflationary ===
Let $T \subseteq S$.
Let $t \in T$.
Then since $T \subseteq S$, $t \in S$ by the definition of subset.
Since $\preceq$ is reflexive, $t \preceq t$.
Thus by the definition of upper closure, $t \in T^\succeq$.
Since this holds for all $t \in T$, $T \subseteq T^\succeq$.
Since this holds for all $T \subseteq S$:
:$\cdot^\succeq$ is inflationary.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $U \subseteq S$.
{{TFAE|def = Upper Section}}

Proof:
=== Definition 1 implies Definition 2 ===
Suppose that:
:$\forall u \in U: \forall s \in S: u \preceq s \implies s \in U$
Let $k \in U^\succeq$.
Then by the definition of upper closure, there is some $u \in U$ such that $u \preceq k$.
Since $k \in U^\succeq \subseteq S$, the premise proves that $k \in U$.
Since this holds for all $k \in U^\succeq$, it follows that:
: $U^\succeq \subseteq U$
{{qed|lemma}}
Theorem: Topological Closure is Closure Operator

The topological closure operator is a closure operator.

Proof:
=== Extensive ===
Follows from Set is Subset of its Topological Closure.
Theorem: Reflexive Closure is Closure Operator

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

Proof:
Let $\QQ$ be the set of reflexive relations on $S$.
By Intersection of Reflexive Relations is Reflexive, the intersection of any subset of $\QQ$ is in $Q$.
By the definition of reflexive closure as the intersection of reflexive supersets:
:The reflexive closure of a relation $\RR$ on $S$ is the intersection of elements of $\QQ$ that contain $S$.
From Closure Operator from Closed Sets we conclude that reflexive closure is a closure operator.
{{qed}}
Theorem: Reflexive Closure is Closure Operator

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

Proof:
=== Reflexive Closure is Inflationary ===
{{:Reflexive Closure is Inflationary}}{{qed|lemma}}
=== Reflexive Closure is Order Preserving ===
{{:Reflexive Closure is Order Preserving}}{{qed|lemma}}
=== Reflexive Closure is Idempotent ===
{{:Reflexive Closure is Idempotent}}{{qed|lemma}}
Thus by the definition of closure operator, reflexive closure is a closure operator.
{{qed}}
Theorem: Set Closure is Smallest Closed Set/Closure Operator

Let $S$ be a set.
Let $\cl: \powerset S \to \powerset S$ be a closure operator.
Let $T \subseteq S$.
Then $\map \cl T$ is the smallest closed set (with respect to $\cl$) containing $T$ as a subset.

Proof:
By definition, $\map \cl T$ is closed.
Let $C$ be closed.
Let $T \subseteq C$.
By the definition of closure operator, $\cl$ is $\subseteq$-increasing.
So:
:$\map \cl T \subseteq \map \cl C$
Since $C$ is closed, $\map \cl C = C$.
So:
:$\map \cl T \subseteq C$
Thus $\map \cl T$ is the smallest closed set containing $T$ as a subset.
{{qed}}
Category:Closure Operators
Category:Set Closure is Smallest Closed Set
rgb5hevh3a910j1evzkrqqrzjppg3ey
Theorem: Equivalence of Definitions of Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $U \subseteq S$.
{{TFAE|def = Lower Section}}

Proof:
We are required to show that the following are equivalent:
{{begin-axiom}}
{{axiom | n = 1
        | m = \forall l \in L: \forall s \in S: s \preceq l \implies s \in L
}}
{{axiom | n = 2
        | m = L^\preceq \subseteq L
}}
{{axiom | n = 3
        | m = L^\preceq = L
}}
{{end-axiom}}
By the Duality Principle, it suffices to prove that:
:$(1^*)$, $(2^*)$ and $(3^*)$ are equivalent
where these are the dual statements of $(1)$, $(2)$ and $(3)$, respectively.
By Dual Pairs, it can be seen that these dual statements are as follows:
{{begin-axiom}}
{{axiom | n = 1^*
        | m = \forall l \in L: \forall s \in S: l \preceq s \implies s \in L
}}
{{axiom | n = 2^*
        | m = L^\succeq \subseteq L
}}
{{axiom | n = 3^*
        | m = L^\succeq = L
}}
{{end-axiom}}
Their equivalence is proved on Equivalence of Definitions of Upper Section.
{{qed}}
Category:Lower Sections
gnr5bkd3bz4d3j9zqeq8zon2u70eb1l
Theorem: Convergent Series of Natural Numbers

Let $\sequence {a_n}_{n \mathop \in \N}$ be a sequence of natural numbers.
Then the following are equivalent:
$(1): \quad \ds \sum_{n \mathop = 1}^\infty a_n$ converges
$(2): \quad \exists N \in \N: \forall n \ge N: a_n = 0$
That is, $\ds \sum_{n \mathop = 1}^\infty a_n$ converges {{iff}} only finitely many of the $a_n$ are non-zero.

Proof:
$(1) \implies (2)$:
Suppose that there is an infinite subsequence $\sequence {a_{n_k} }_{k \mathop \in \N}$ such that for each $k$, $a_{n_k} \ne 0$.
For $N \in \N$ let 
:$\ds s_N = \sum_{n \mathop = 1}^N a_n$
To show that $s_N$ diverges it suffices to show that:
:$\forall M > 0: \exists N \in \N : \forall n > N : \size {s_n} > M$
Since for each $n$, $a_n \ge 0$, $s_N$ is a positive increasing sequence in $N$.
Therefore it suffices to show that:
:$\forall M > 0: \exists N \in \N: s_N > M$
Fix $M > 0$.
Let $k$ be any positive integer such that $n_k > M$.
Then we have:
{{begin-eqn}}
{{eqn | l = s_{n_k}
      | r = \sum_{n \mathop = 1}^{n_k} a_n
}}
{{eqn | r =\sum_{n \mathop = 1}^{n_k} 1
      | o = \ge
      | c = as the $a_n$ are positive and non-zero
}}
{{eqn | r = n_k
      | c =
}}
{{eqn | r = M
      | c = By the choice of $n_k$
}}
{{end-eqn}}
Therefore the sequence $s_N$ diverges.
$(2) \implies (1)$:
Suppose there exists $N > 0$ such that $a_n = 0$ for all $n > N$.
Then we have, for all $L > N$:
:$\ds s_L = \sum_{n \mathop = 1}^L a_n = \sum_{n \mathop = 1}^N a_n = s_N$
In particular, for any $\epsilon > 0$ and all $L > N$:
:$\size {s_L - s_N} = 0 < \epsilon$
Therefore the sequence converges to $s_N$.
{{Qed}}
Category:Natural Numbers
Category:Series
bgmoo49o9gfc32ts6kvaromvevaasb3
Theorem: Closure Operator from Closed Sets

Let $S$ be a set.
Let $\CC$ be a set of subsets of $S$.
Let $\CC$ be closed under arbitrary intersections:
:$\forall \KK \in \powerset \CC: \bigcap \KK \in \CC$
where $\bigcap \O$ is taken to be $S$.
Define $\cl: \powerset S \to \CC$ by letting:
:$\map \cl T = \bigcap \set {C \in \CC: T \subseteq C}$
Then $\cl$ is a closure operator whose closed sets are the elements of $\CC$.

Proof:
First we will show that $\cl$ is a closure operator.
Theorem: Intersection is Decreasing

Let $U$ be a set.
Let $\FF$ and $\GG$ be sets of subsets of $U$.
Then $\FF \subseteq \GG \implies \bigcap \GG \subseteq \bigcap \FF$, where by convention $\bigcap \O = U$.
That is, $\bigcap$ is a decreasing mapping from $\struct {\powerset {\powerset U}, \subseteq}$ to $\struct {\powerset U, \subseteq}$, where $\powerset U$ is the power set of $U$.

Proof:
Let $\FF \subseteq \GG$.
Let $x \in \bigcap \GG$.
Then for each $S \in \FF$, $S \in \GG$.
By the definition of intersection, $x \in S$.
Since this holds for all $S \in \FF$, $x \in \bigcap \FF$.
Since this holds for all $ x \in \bigcap \GG$:
:$\bigcap \GG \subseteq \bigcap \FF$
{{qed}}
Category:Set Intersection
sb5cyeovtz4me3xrwtp8o6ei3edv0jo
Theorem: Open Ray is Open in GO-Space/Definition 2

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 2.
That is:
:Let $\struct {S, \preceq}$ be a totally ordered set.
:Let $\struct {S, \tau}$ be a topological space.
Let there be:
:a linearly ordered space $\struct {S', \preceq', \tau'}$
and:
:a mapping $\phi: S \to S'$ which is both:
::a $\preceq$-$\preceq'$ order embedding
:and:
::a $\tau$-$\tau'$ topological embedding.
Let $p \in S$.
Then:
:$p^\prec$ and $p^\succ$ are $\tau$-open
where:
:$p^\prec$ is the strict lower closure of $p$
:$p^\succ$ is the strict upper closure of $p$.

Proof:
We will prove that $p^\succ$ is open.
{{explain|follow by duality how?}}
That $p^\prec$ is open will follow by duality.
By Inverse Image under Order Embedding of Strict Upper Closure of Image of Point:
:$\map {\phi^{-1} } {\map \phi p^\succ} = p^\succ$
:$\map \phi p^\succ$ is an open ray in $S'$
Therefore $\tau'$-open by the definition of the order topology.
{{explain|What exactly is $\tau'$-open here?}}
Since $\phi$ is a topological embedding, it is continuous.
Thus $p^\succ$ is $\tau$-open.
{{qed}}
Theorem: Union is Increasing

Let $U$ be a set.
Let $\FF$ and $\GG$ be sets of subsets of $U$.
Then $\FF \subseteq \GG \implies \bigcup \FF \subseteq \bigcup \GG$.
That is, $\bigcup$ is an increasing mapping from $\struct {\powerset {\powerset U}, \subseteq}$ to $\struct {\powerset U, \subseteq}$, where $\powerset U$ is the power set of $U$.

Proof:
Let $\FF \subseteq \GG$.
Let $x \in \bigcup \FF$.
Then by the definition of union:
:$\exists S \in \FF: x \in S$
By the definition of subset:
:$S \in \GG$
Thus by the definition of union:
:$x \in \bigcup \GG$
Since this holds for all $x \in \bigcup \FF$:
:$\bigcup \FF \subseteq \bigcup \GG$
{{qed}}
Category:Set Union
mdszcpsshmb7r81pae4ehuq3zuyotjp
Theorem: Set Intersection is Idempotent/Indexed Family

Let $\family {F_i}_{i \mathop \in I}$ be a non-empty indexed family of sets.
Suppose that all the sets in the $\family {F_i}_{i \mathop \in I}$ are the same.
That is, suppose that for some set $S$:
:$\forall i \in I: F_i = S$
Then:
:$\ds \bigcap_{i \mathop \in I} F_i = S$
where $\ds \bigcap_{i \mathop \in I} F_i$ is the intersection of $\family {F_i}_{i \mathop \in I}$.

Proof:
First we show that:
:$\ds \bigcap_{i \mathop \in I} F_i \subseteq S$
Let $x \in \ds \bigcap_{i \mathop \in I} F_i$.
Since $I$ is non-empty, it has an element $k$.
By the definition of intersection, $x \in F_k$.
By the premise, $F_k = S$, so $x \in S$.
Since this holds for all $x \in \ds \bigcap_{i \mathop \in I} F_i$:
:$\ds \bigcap_{i \mathop \in I} F_i \subseteq S$
Next we show that:
:$\ds S \subseteq \bigcap_{i \mathop \in I} F_i$
Let $x \in S$.
Then for all $i \in I$, $F_i = S$, so $x \in F_i$.
Thus by the definition of intersection:
:$x \in \ds \bigcap_{i \mathop \in I} F_i$
Since this holds for all $x \in S$:
:$S \subseteq \ds \bigcap_{i \mathop \in I} F_i$
By definition of set equality:
:$\ds \bigcap_{i \mathop \in I} F_i = S$
{{qed}}
Category:Set Intersection
Category:Indexed Families
Category:Examples of Idempotence
0f44x27gk0sn8suv0rvn7qysv05fvmt
Theorem: Factor Principles/Disjunction on Left/Formulation 1/Proof 1

:$p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q} }}
{{Premise|1|p \implies q}}
{{TheoremIntro|2|r \implies r|Law of Identity: Formulation 2}}
{{SequentIntro|3|1|\paren {r \lor p} \implies \paren {r \lor q}|2, 1|Constructive Dilemma}}
{{EndTableau}}
{{qed}}
Theorem: Constructive Dilemma for Join Semilattices

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $a, b, c, d \in S$.
Let $a \preceq b$.
Let $c \preceq d$.
Then $\paren {a \vee c} \preceq \paren {b \vee d}$.

Proof:
By Join Semilattice is Ordered Structure, $\preceq$ is compatible with $\vee$.
By the definition of ordering, $\preceq$ is transitive.
Thus the theorem holds by Operating on Transitive Relationships Compatible with Operation.
{{qed}}
Category:Lattice Theory
gsg75kiusqg9sajkk7sl9l8iitilbgy
Theorem: Praeclarum Theorema for Meet Semilattices

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.
{{qed}}