avewright/proofwiki-math huggingface dataset:
Theorem: Image of Closure Operator Inherits Infima

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $f$ be a closure operator on $L$.
Then $R = \struct {f \sqbrk S, \precsim}$ inherits infima,
where
:$\mathord \precsim = \mathord \preceq \cap \paren {f \sqbrk S \times f \sqbrk S}$
:$f \sqbrk S$ denotes the image of $f$.

Proof:
Let $X$ be subset of $f \sqbrk S$ such that
:$X$ admits an infimum in $L$.
By Closure Operator does not Change Infimum of Subset of Image:
:$\map f {\inf_L X} = \inf_L X$
By definition of image of mapping:
:$\inf_L X \in f \sqbrk S$
Thus by Infimum in Ordered Subset:
:$X$ admits an infimum in $R$ and $\inf_R X = \inf_L X$
{{qed}}
Theorem: Necessary Condition for Integral Functional to have Extremum for given function/Lemma

Let $\map \alpha x, \map \beta x$ be real functions.
Let $\map \alpha x, \map \beta x$ be continuous on $\closedint a b$.
Let:
:$\forall \map h x \in C^1: \ds \int_a^b \paren {\map \alpha x \map h x + \map \beta x \map {h'} x} \rd x = 0$
subject to the boundary conditions:
:$\map h a = \map h b = 0$
Then $\map \beta x$ is differentiable.
Furthermore:
:$\forall x \in \closedint a b: \map {\beta'} x = \map \alpha x$

Proof:
Using Integration by Parts allows us to factor out $\map h x$:
{{begin-eqn}}
{{eqn | l = \int_a^b \paren {\map \alpha x \map h x + \map \beta x \map {h'} x} \rd x
      | r = \int_a^b \map \alpha x \map h x \rd x + \int_a^b \map \beta x \rd \map h x
      | c = where $\d \map h x = \map {h'} x \rd x$
}}
{{eqn | r = \int_a^b \map \alpha x \map h x \rd x + \bigintlimits {\map \beta x \map h x} a b - \int_a^b \map h x \rd \map \beta x
      | c = Integration by Parts
}}
{{eqn | r = \int_a^b \paren {\map \alpha x - \map {\beta'} x} \map h x \rd x
      | c = as $\map h a = 0$, $\map h b = 0$
}}
{{end-eqn}}
Hence the problem has been reduced to:
:$\ds \int_a^b \paren {\map \alpha x - \map {\beta'} x} \map h x \rd x = 0$
Since If Definite Integral of $\map a x \map h x$ vanishes for any $C^0 \map h x$ then $C^0 \map a x$ vanishes, the conclusion is that in the considered interval $\closedint a b$ it holds that:
:$\map \alpha x = \map {\beta'} x$
{{qed}}
Theorem: If Definite Integral of a(x)h(x) vanishes for any C^0 h(x) then C^0 a(x) vanishes

Let $\map \alpha x$ be a continuous real function on the closed real interval $\closedint a b$.
Let $\ds \int_a^b \map \alpha x \map h x \rd x = 0$ for every real function $\map h x \in C^0 \closedint a b$ such that $\map h a = 0$ and $\map h b = 0$.
where $C^0 \closedint a b$ means continuous functions on $\closedint a b$.
Then $\map \alpha x = 0$ for all $x \in \closedint a b$.

Proof:
{{AimForCont}} the real function $\map \alpha x$ is nonzero at some point in $\closedint a b$ for some arbitrary $\map h x$. 
Due to belonging to $C^0$ it is also nonzero in some interval $\closedint {x_1} {x_2}$ contained in $\closedint a b$.
Let us choose $\map h x$ to be of a specific form, while still satisfying the requirements in the statement of the theorem:
:$\map h x = \begin {cases}
\map \sgn {\map \alpha x} \paren {x - x_1} \paren {x_2 - x} & : x \in \closedint {x_1} {x_2} \\
0 & : x \notin \closedint {x_1} {x_2}
\end {cases}$
Then:
:$\ds \int_a^b \map \alpha x \map h x \rd x = \int_{x_1}^{x_2} \size {\map \alpha x} \paren {x - x_1} \paren {x_2 - x} \rd x$
where we used the fact that:
:$\map \alpha x = \map \sgn {\map \alpha x} \size {\map \alpha x}$
as well as:
:$\map {\sgn^2} x = 1$ if $x \ne 0$ and $x \in \R$.
The integrand is positive for $x \in \closedint {x_1} {x_2}$, whence the integral is positive.
However, that contradicts the condition on the integral in the statement of the theorem.
Thus, with the provided assumption the condition for the integral does not hold for all $\map h x$ with aforementioned conditions.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Closure Operator does not Change Infimum of Subset of Image

Let $L = \left({S, \preceq}\right)$ be an ordered set.
Let $c: S \to S$ be a closure operator on $L$.
Let $X$ be a subset of $c\left[{S}\right]$ such that
:$X$ admits an infimum,
where $c\left[{S}\right]$ denotes the image of $c$.
Then $\inf X = c\left({\inf X}\right)$

Proof:
We will prove that
:$c\left({\inf X}\right)$ is lower bound for $X$.
Let $x \in X$.
By definition of subset:
:$x \in c\left[{S}\right]$
By definition of image of mapping:
:$\exists y \in S: x = c\left({y}\right)$
By definition of closure operator/idempotent:
:$x = c\left({x}\right)$
By definition of infimum:
:$\inf X$ is lower bound for $X$.
By definition of lower bound:
:$\inf X \preceq x$
Thus by definition of closure operator/increasing:
:$c\left({\inf X}\right) \preceq x$
{{qed|lemma}}
By definition of infimum:
:$c\left({\inf X}\right) \preceq \inf X$
By definition of closure operator/inflationary:
:$c\left({\inf X}\right) \succeq \inf X$
Thus by definition of antisymmetry:
:$c\left({\inf X}\right) = \inf X$
{{qed}}
Theorem: Infimum in Ordered Subset

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.
Let $X \subseteq T$ such that
:$X$ admits an infimum in $L$.
Then $\inf_L X \in T$ {{iff}}
:$X$ admits an infimum in $R$ and $\inf_R X = \inf_L X$

Proof:
By definition of ordered subset:
:$T \subseteq S$
and
:$\forall x, y \in T: x \preceq' y \iff x \preceq y$
Theorem: Operator Generated by Closure System is Closure Operator

Let $L = \left({X, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Let $S = \left({T, \precsim}\right)$ be a closure system of $L$.
Then $\operatorname{operator}\left({S}\right)$ is closure operator,
where $\operatorname{operator}\left({S}\right)$ denotes the operator generated by $S$.

Proof:
Define $f = \operatorname{operator}\left({S}\right)$.
Theorem: Image of Operator Generated by Closure System is Set of Closure System

Let $L = \struct {X, \vee, \wedge, \preceq}$ be a complete lattice.
Let $S = \struct {T, \precsim}$ be a closure system of $L$.
Then $\map {\operatorname {operator} } S \sqbrk X = T$
where $\map {\operatorname {operator} } S$ denotes the operator generated by $S$.

Proof:
Define $f = \map {\operatorname {operator} } S$.
Theorem: Regular Icosahedron as Pentagonal Antiprism with Pyramidal Endcaps

The regular icosahedron can be considered as a regular pentagonal antiprism with two regular pentagonal pyramid as end caps.
{{stub|Need to construct an icosahedron.}}

Proof:
{{ProofWanted|Probably get away with a drawing here.}}
Theorem: Construction of Rhombic Dodecahedron

The rhombic dodecahedron can be constructed as follows:
Take a cube $K$ embedded in $3$-dimensional space.
Place $6$ more cubes, each congruent with $K$, so that one face of each coincides with a different face of $K$.
Join the vertices of $K$ to the centers of the adjacent cubes to describe square pyramids whose apices are the centers of the adjacent cubes and whose bases are the faces of $K$.
The polyhedron formed by the $6$ square pyramids so formed, together with $K$, is a rhombic dodecahedron.

Proof:
{{ProofWanted|Needs a diagram}}
Theorem: Conditions for C^1 Smooth Solution of Euler's Equation to have Second Derivative

Let $\map y x:\R \to \R$ be a real function.
Let $\map F {x, y, y'}:\R^3 \to \R$ be a real function.
Suppose $\map F {x, y, y'}$ has continuous first and second derivatives {{WRT|Differentiation}} all its arguments.
Suppose $y$ has a continuous first derivative and satisfies Euler's equation: 
:$F_y - \dfrac \d {\d x} F_{y'} = 0$
Suppose:
:$\map {F_{y' y'} } {x, \map y x, \map y x'} \ne 0$
Then $\map y x$ has continuous second derivatives.

Proof:
Consider the difference
{{begin-eqn}}
{{eqn | l = \Delta F_{y'}
      | r = \map F {x + \Delta x, y + \Delta y, y' + \Delta y'} - \map F {x, y, y'}
      | c = 
}}
{{eqn | r = \Delta x \overline F_{y' x} + \Delta y \overline F_{y'y} + \Delta y' \overline F_{y'y'}
      | c = Multivariate Mean Value Theorem
}}
{{end-eqn}}
Overbar indicates that derivatives are evaluated along certain intermediate curves.
{{Explain|intermediate curves}}
Divide $\Delta F_{y'} $ by $\Delta x$ and consider the limit $\Delta x \to 0$:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta F_{y'} } {\Delta x} = \lim_{\Delta x \mathop \to 0} \paren {\overline F_{y'x} + \frac {\Delta y} {\Delta x} \overline F_{y' y} + \frac {\Delta y'} {\Delta x} \overline F_{y'y'} }$
Existence of second derivatives and continuity of $F$ is guaranteed by conditions of the theorem:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta F_{y'} } {\Delta x} = F_{y' x}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' x} = F_{y' x}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' y} = F_{y' y}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' y} = F_{y'y'}$
Similarly:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta y} {\Delta x} =  y'$
By Product Rule for Limits of Real Functions, it follows that:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta y'} {\Delta x} = y''$
Hence $y''$ exists wherever $F_{y' y'} \ne 0$.
Euler's equation and continuity of necessary derivatives of $F$ and $y$ implies that $y''$ is continuous.
{{Explain|explain how barred functionals become unbarred}}
Theorem: Recurring Parts of Multiples of One Thirteenth

The multiples of $\dfrac 1 {13}$ from $\dfrac 1 {13}$ to $\dfrac {12} {13}$ can be divided into two sets of equal size:
:one where the digits of the recurring part consists of a cyclic permutation of $076923$
:one where the digits of the recurring part consists of a cyclic permutation of $153846$.
:300px

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {13}
      | r = 0 \cdotp 076923 \, 076923 \ldots
      | c = 
}}
{{eqn | l = \dfrac 2 {13}
      | r = 0 \cdotp 153846 \, 153846 \ldots
      | c = 
}}
{{eqn | l = \dfrac 3 {13}
      | r = 0 \cdotp 230796 \, 230796 \ldots
      | c = 
}}
{{eqn | l = \dfrac 4 {13}
      | r = 0 \cdotp 307692 \, 307692 \ldots
      | c = 
}}
{{eqn | l = \dfrac 5 {13}
      | r = 0 \cdotp 384615 \, 384615 \ldots
      | c = 
}}
{{eqn | l = \dfrac 6 {13}
      | r = 0 \cdotp 461538 \, 461538 \ldots
      | c = 
}}
{{eqn | l = \dfrac 7 {13}
      | r = 0 \cdotp 538461 \, 538461 \ldots
      | c = 
}}
{{eqn | l = \dfrac 8 {13}
      | r = 0 \cdotp 615384 \, 615384 \ldots
      | c = 
}}
{{eqn | l = \dfrac 9 {13}
      | r = 0 \cdotp 692307 \, 692307 \ldots
      | c = 
}}
{{eqn | l = \dfrac {10} {13}
      | r = 0 \cdotp 769230 \, 769230 \ldots
      | c = 
}}
{{eqn | l = \dfrac {11} {13}
      | r = 0 \cdotp 846153 \, 846153 \ldots
      | c = 
}}
{{eqn | l = \dfrac {12} {13}
      | r = 0 \cdotp 923076 \, 923076 \ldots
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Twelve Factorial plus One is divisible by 13 Squared

:$12! + 1$ is divisible by $13^2$.

Proof:
By calculuation:
{{begin-eqn}}
{{eqn | l = 12! + 1
      | r =  479 \, 001 \, 601
      | c = 
}}
{{eqn | r = 2 \, 834 \, 329 \times 13 \times 13
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Torus can be cut into 13 Pieces with 3 Plane Cuts

A torus can be cut into as many as $13$ separate pieces by $3$ plane cuts.

Proof:
{{ProofWanted|Lots of background work needed.}}
Theorem: Operator Generated by Image of Closure Operator is Closure Operator

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $c: S \to S$ be a closure operator on $L$.
Then $\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } = c$
where
:$\mathord \precsim = \mathord \preceq \cap \paren {c \sqbrk S \times c \sqbrk S}$
:$\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} }$ denotes the operator generated by $\struct {c \sqbrk S, \precsim}$

Proof:
Let $x \in S$.
By definition of closure operator/inflationary:
:$x \preceq \map c x$
By definition of upper closure of element:
:$\map c x \in x^\succeq$
By definition of image of mapping:
:$\map c x \in c \sqbrk S$
By definition of intersection:
:$\map c x \in x^\succeq \cap c \sqbrk S$
By definitions of infimum and lower bound:
:$\map {\inf_L} {x^\succeq \cap c \sqbrk S} \preceq \map c x$
We will prove that
:$\map c x$ is lower bound for $x^\succeq \cap c \sqbrk S$
Let $y \in x^\succeq \cap c \sqbrk S$
By definition of intersection:
:$y \in x^\succeq$ and $y \in c \sqbrk S$
By definition of image of mapping:
:$\exists z \in S: y = \map c z$
By definition of closure operator/idempotent:
:$y = \map c y$
By definition of upper closure of element:
:$x \preceq y$
Thus by definition of closure operator/increasing:
:$\map c x \preceq y$
{{qed|lemma}}
By definition of infimum:
:$\map c x \preceq \map {\inf_L} {x^\succeq \cap c \sqbrk S}$
By definition of antisymmetry:
:$\map c x = \map {\inf_L} {x^\succeq \cap c \sqbrk S}$
Thus by definition of operator generated by $\struct {c \sqbrk S, \precsim}$:
:$\map {\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } } x = \map c x$
Hence by Equality of Mappings:
:$\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } = c$
{{qed}}
Theorem: If Double Integral of a(x, y)h(x, y) vanishes for any C^2 h(x, y) then C^0 a(x, y) vanishes

Let $\map \alpha {x, y}$, $\map h {x, y}$ be functions in $\R$.
{{mistake|should that be $\R^2$?}}
Let $\alpha \in C^0$ in a closed region $R$ whose boundary is $\Gamma$.
Let $h \in C^2$ in $R$ and $h = 0$ on $\Gamma$.
Let:
:$\ds \iint_R \map \alpha {x, y} \map h {x, y} \rd x \rd y = 0$
Then $\map \alpha {x, y}$ vanishes everywhere in $R$.

Proof:
{{AimForCont}} $\map \alpha {x, y}$ is nonzero at some point in $R$.
Then $\map \alpha {x, y}$ is also nonzero in some disk $D$ such that:
:$\paren {x - x_0}^2 + \paren {y - y_0}^2 \le \epsilon^2$
Suppose:
:$\map h {x, y} = \map \sgn {\map \alpha {x, y} } \paren {\epsilon^2 - \paren {x - x_0}^2 + \paren {y - y_0}^2}^3$ 
in this disk and $0$ elsewhere.
Thus $\map h {x, y}$ satisfies conditions of the theorem.
However:
:$\ds \iint_R \map \alpha {x, y} \map h {x, y} \rd x \rd y = \iint_D \size {\map \alpha {x, y} } \paren {\epsilon^2 - \paren {x - x_0}^2 + \paren {y - y_0}^2}^3 \ge 0$
Hence the result, by Proof by Contradiction.
{{qed}}
Theorem: Pell's Equation/Examples/13

:$x^2 - 13 y^2 = 1$
has the smallest positive integral solution:
:$x = 649$
:$y = 180$

Proof:
From Continued Fraction Expansion of $\sqrt {13}$:
:$\sqrt {13} = \sqbrk {3, \sequence {1, 1, 1, 1, 6} }$
The cycle is of length $5$.
By Solution of Pell's Equation, the only solutions of $x^2 - 13 y^2 = 1$ are:
:${p_{5 r} }^2 - 13 {q_{5 r} }^2 = \paren {-1}^{5 r}$
for $r = 1, 2, 3, \ldots$
When $r = 1$ this gives:
:${p_5}^2 - 13 {q_5}^2 = -1$
which is not the solution required.
When $r = 2$ this gives:
:${p_{10} }^2 - 13 {q_{10} }^2 = 1$
From Convergents of Continued Fraction Expansion of $\sqrt {13}$:
:$p_{10} = 649$
:$q_{10} = 180$
although on that page the numbering goes from $p_0$ to $p_9$, and $q_0$ to $q_9$.
{{qed}}
Theorem: Pell's Equation/Examples/29

:$x^2 - 29 y^2 = 1$
has the smallest positive integral solution:
:$x = 9801$
:$y = 1820$

Proof:
From Continued Fraction Expansion of $\sqrt {29}$:
:$\sqrt {29} = \sqbrk {5, \sequence {2, 1, 1, 2, 10} }$
The cycle is of length is $5$.
By Solution of Pell's Equation, the only solutions of $x^2 - 29 y^2 = 1$ are:
:${p_{5 r} }^2 - 29 {q_{5 r} }^2 = \paren {-1}^{5 r}$
for $r = 1, 2, 3, \ldots$
When $r = 1$ this gives:
:${p_5}^2 - 29 {q_5}^2 = -1$
which is not the solution required.
When $r = 2$ this gives:
:${p_{10} }^2 - 29 {q_{10} }^2 = 1$
From Convergents of Continued Fraction Expansion of $\sqrt {29}$:
:$p_{10} = 9801$
:$q_{10} = 1820$
although on that page the numbering goes from $p_0$ to $p_9$, and $q_0$ to $q_9$.
{{qed}}
Theorem: Ordered Set of Closure Operators and Dual Ordered Set of Closure Systems are Isomorphic

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Then $\operatorname{Closure}\left({L}\right)$ and $\operatorname{ClSystems}\left({L}\right)^{-1}$ are order isomorphic
where
:$\operatorname{Closure}\left({L}\right)$ denotes the ordered set of closure operators of $L$,
:$\operatorname{ClSystems}\left({L}\right)$ denotes the ordered set of closure systems oj $L$,
:$\operatorname{ClSystems}\left({L}\right)^{-1}$ denotes the dual to $\operatorname{ClSystems}\left({L}\right)$.

Proof:
By definition of ordered set of closure operators:
:$\operatorname{Closure}\left({L}\right) = \left({X, \preceq'}\right)$
where
:$X$ is the set of all closure operators on $L$,
:for all closure operators $f, g$ on $L$: $f \preceq' g \iff f \preceq g$
:$\preceq$ denotes the ordering on mappings.
By definition of ordered set of closure systems:
:$\operatorname{ClSystems}\left({L}\right) = \left({Y, \precsim}\right)$
where
:$Y$ is the set of all closure systems on $L$,
:for all closure systems $s_1 = \left({T_1, \preceq_1}\right)$, $s_2 = \left({T_2, \preceq_2}\right)$ on $L$: $s_1 \precsim s_2 \iff T_1 \subseteq T_2$
Define $F:X \to Y$ by Image of Closure Operator Inherits Infima:
:for all closure operators $f$ on $L$: $F\left({f}\right) = \left({f\left[{S}\right], \mathord\preceq \cap \left({f\left[{S}\right] \times f\left[{S}\right]}\right)}\right)$
By Operator Generated by Closure System is Closure Operator and Image of Operator Generated by Closure System is Set of Closure System:
:$F$ is a surjection.
By Ordering on Closure Operators iff Images are Including:
:$F$ is an order embedding.
Thue by definition:
:$F$ is an order isomorphism.
{{qed}}
Theorem: Supremum in Ordered Subset

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.
Let $X \subseteq T$ such that
:$X$ admits an supremum in $L$.
Then $\sup_L X \in T$ {{iff}}
:$X$ admits an supremum in $R$ and $\sup_R X = \sup_L X$

Proof:
This follows by {{mutatis}} of the proof of Infimum in Ordered Subset.
{{qed}}
Theorem: Partial Denominators of Continued Fraction Expansion of Irrational Square Root

Let $n \in \Z$ such that $n$ is not a square.
Let the continued fraction expansion of $\sqrt n$ be expressed as:
:$\sqbrk {a_0, a_1, a_2, \ldots}$
Then the partial denominators of this continued fraction expansion can be calculated as:
:$a_r = \floor {\dfrac {\floor {\sqrt n} + P_r} {Q_r} }$
where:
:<nowiki>$P_r = \begin{cases} 0 & : r = 0 \\
a_{r - 1} Q_{r - 1} - P_{r - 1} & : r > 0 \\
\end{cases}$</nowiki>
:<nowiki>$Q_r = \begin{cases} 1 & : r = 0 \\
\dfrac {n - {P_r}^2} {Q_{r - 1} } & : r > 0 \\
\end{cases}$</nowiki>

Proof:
The proof proceeds by strong induction.
For all $r \in \Z_{\ge 0}$, let $\map P r$ be the proposition:
:$a_r = \floor {\dfrac {\floor {\sqrt n} + P_r} {Q_r} }$
where:
:<nowiki>$P_r = \begin{cases} 0 & : r = 0 \\
a_{r - 1} Q_{r - 1} - P_{r - 1} & : r > 0 \\
\end{cases}$</nowiki>
:<nowiki>$Q_r = \begin{cases} 1 & : r = 0 \\
\dfrac {n - {P_r}^2} {Q_{r - 1} } & : r > 0 \\
\end{cases}$</nowiki>
Theorem: Operator Generated by Closure System Preserves Directed Suprema iff Closure System Inherits Directed Suprema

Let $L = \struct {X, \vee, \wedge, \preceq}$ be a complete lattice.
Let $S = \struct {Y, \precsim}$ be a closure system on $L$.
Then $\map {\operatorname {operator} } S$ preserves directed suprema
{{iff}} $S$ inherits directed suprema.
where $\map {\operatorname {operator} } S$ denotes the operator generated by $S$.

Proof:
=== Sufficient Condition ===
Assume that $\map {\operatorname {operator} } S$ preserves directed suprema.
Let $Z$ be directed subset of $Y$ such that
:$Z$ admits a supremum in $L$.
By Image of Operator Generated by Closure System is Set of Closure System:
:$\map {\operatorname {operator} } S \sqbrk X = Y$
By Operator Generated by Closure System is Closure Operator:
:$\map {\operatorname {operator} } S$ is closure operator.
By definition of closure operator/idempotent:
:$\map {\operatorname {operator} } S \sqbrk Z = Z$
By definitions of Definition:Mapping Preserves Supremum/Directed and Definition:Mapping Preserves Supremum/Subset:
:$\sup_L Z = \map {\map {\operatorname {operator} } S} {\sup_L Z}$
Thus by definition of image of mapping:
:$\sup_L Z \in Y$
{{qed|lemma}}
Theorem: Closure Operator Preserves Directed Suprema iff Image of Closure Operator Inherits Directed Suprema

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $h: S \to S$ be a closure operator on $L$.
Then $h$ preserves directed suprema
{{iff}} $\struct {h \sqbrk S, \precsim}$ inherits directed suprema.
where
:$h \sqbrk S$ denotes the image of $h$,
:$\mathord\precsim = \mathord\preceq \cap \paren {h \sqbrk S \times h \sqbrk S}$

Proof:
By Operator Generated by Image of Closure Operator is Closure Operator:
:$\map {\operatorname{operator} } {\struct {h \sqbrk S, \precsim} } = h$
where $\map {\operatorname{operator} } {\struct {h \sqbrk S, \precsim} }$ denotes the operator generated by $\struct {h \sqbrk S, \precsim}$
Hence the result holds by Operator Generated by Closure System Preserves Directed Suprema iff Closure System Inherits Directed Suprema.
{{qed}}
Theorem: Infimum Precedes Coarser Infimum

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Let $X, Y$ be subsets of $S$ such that
:$Y$ is coarser than $X$.
Then $\inf X \preceq \inf Y$
where $\inf X$ denotes the infimum of $X$.

Proof:
We will prove that
:$\inf X$ is lower bound for $Y$.
Let $x \in Y$.
By definition of coarser subset:
:$\exists y \in X: y \preceq x$
By definitions of infimum and lower bound:
:$\inf X \preceq y$
Thus by definition of transitivity:
:$\inf X \preceq x$
{{qed|lemma}}
Hence by definition of infimum:
:$\inf X \preceq \inf Y$
{{qed}}
Theorem: Uniform Prism is Semiregular Polyhedron

Let $\PP$ be a uniform prism whose bases are specifically not square.
Then $\PP$ is a semiregular polyhedron.

Proof:
{{Recall|Semiregular Polyhedron}}
{{:Definition:Semiregular Polyhedron}}
Let $\PP$ be a uniform prism.
By definition, $\PP$ is regular.
Hence the bases of $\PP$ are regular polygons.
Also by definition, the lateral faces of $\PP$ are square so {{afortiori}} regular polygons.
Suppose the bases of $\PP$ are square.
Then all the faces of $\PP$ are square.
Thus $\PP$ would be a cube.
Thus, because all faces of $\PP$ are congruent, $\PP$ is not a semiregular polyhedron, by definition.
Hence the restriction on $\PP$.
Finally, from Uniform Prism is Isogonal, we have that $\PP$ is isogonal.
Hence the result.
{{qed}}
Theorem: Uniform Antiprism is Semiregular Polyhedron

Let $\PP$ be a uniform antiprism whose bases are specifically not (equilateral) triangles.
Then $\PP$ is a semiregular polyhedron.

Proof:
{{Recall|Semiregular Polyhedron}}
{{:Definition:Semiregular Polyhedron}}
Let $\PP$ be a uniform antiprism.
By definition, $\PP$ is regular.
Hence the bases of $\PP$ are regular polygons.
Also by definition, the lateral faces of $\PP$ are equilateral triangles so {{afortiori}} regular polygons.
Suppose the bases of $\PP$ are equilateral triangles.
Then all the faces of $\PP$ are equilateral triangles.
Thus $\PP$ would be an octahedron.
Thus, because all faces of $\PP$ are congruent, $\PP$ is not a semiregular polyhedron, by definition.
Hence the restriction on $\PP$.
Finally, from Uniform Antiprism is Isogonal, we have that $\PP$ is isogonal.
Hence the result.
{{qed}}
Theorem: Finer Supremum Precedes Supremum

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Let $X, Y$ be subsets of $S$ such that
:$X$ is finer than $Y$.
Then $\sup X \preceq \sup Y$
where $\sup X$ denotes the supremum of $X$.

Proof:
We will prove that
:$\sup Y$ is upper bound for $X$.
Let $x \in X$.
By definition of finer subset:
:$\exists y \in Y: x \preceq y$
By definitions of supremum and upper bound:
:$y \preceq \sup Y$
Thus by definition of transitivity:
:$x \preceq \sup Y$
{{qed|lemma}}
Hence by definition of supremum:
:$\sup X \preceq \sup Y$
{{qed}}
Theorem: Thirteen Catalan Polyhedra

There exist exactly $13$ distinct Catalan polyhedra:
:Triakis tetrahedron
:Triakis octahedron
:Disdyakis dodecahedron
:Tetrakis hexahedron
:Triakis icosahedron
:Disdyakis triacontahedron
:Pentakis dodecahedron
:Rhombic dodecahedron
:Rhombic triacontahedron
:Deltoidal icositetrahedron
:Deltoidal hexecontahedron
:Pentagonal icositetrahedron
:Pentagonal hexecontahedron

Proof:
By definition, the Catalan polyhedra are the dual polyhedra of the Archimedean polyhedra.
There are $13$ Archimedean polyhedra, and so there are $13$ Catalan polyhedra.
{{ProofWanted|Include links to specific results linking the Archimedean polyhedra with their duals.}}