Closed Elements Uniquely Determine Closure Operator
Specifically, implement the $\mathsf{Pr} \infty \mathsf{fWiki}$ standard symbols for upper and lower closures
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
Theorem
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $f, g: S \to S$ be closure operators on $S$.
Suppose that $f$ and $g$ have the same closed elements.
Then $f = g$.
Proof
Let $x \in S$.
Let $C$ be the set of closed elements of $S$ (with respect to either $f$ or $g$) that succeed $x$.
By Closure is Smallest Closed Successor, $f \left({x}\right)$ and $g \left({x}\right)$ are smallest closed successors of $x$.
That is, $f \left({x}\right)$ and $g \left({x}\right)$ are smallest elements of $C \cap \bar\uparrow x$, where $\bar\uparrow x$ is the upper closure of $x$.
By Smallest Element is Unique, $f \left({x}\right) = g \left({x}\right)$.
Since this holds for all $x \in S$, $f = g$ by Equality of Mappings.
$\blacksquare$
