Lower Topology is Unique

Theorem

Let $T_1 = \left({S, \preceq, \tau_1}\right)$ and $T_2 = \left({S, \preceq, \tau_2}\right)$ be relational structures with lower topologies.

Then:

$\tau_1 = \tau_2$

Proof

Define:

$B := \left\{ {\complement_S \left({x^\succeq}\right): x \in S}\right\}$

where $x^\succeq$ denotes the upper closure of $x$.

Thus:

\(\ds \tau_1\)

\(=\)

\(\ds \tau \left({B}\right)\)

Definition of Topology Generated by Synthetic Sub-Basis

\(\ds \)

\(=\)

\(\ds \tau_2\)

Definition of Topology Generated by Synthetic Sub-Basis

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL19:2