Way Below in Ordered Set of Topology
Theorem
Let $\struct {S, \tau}$ be a topological space.
Let $\struct {\tau, \preceq}$ be an ordered set where $\preceq \mathop = \subseteq \restriction_{\tau \times \tau}$
Let $x, y \in \tau$.
Then:
- $x \ll y$ in $\struct {\tau, \preceq}$
where $\ll$ denotes the way below relation.
Proof
Sufficient Condition
Let
- $x \ll y$
Let $F$ be a set of open subsets of $S$ such that
- $y \subseteq \bigcup F$
By definition of subset:
- $F \subseteq \tau$
By proof of Topology forms Complete Lattice:
- $\sup F = \bigcup F$
By assumption:
- $y \preceq \sup F$
By Topology forms Complete Lattice:
- $\struct {\tau, \preceq}$ is complete lattice.
By Way Below in Complete Lattice:
- $\exists G \in \map {\it Fin} F: x \preceq \sup G$
where $\map {\it Fin} F$ denotes the set of all finite subsets of $F$.
Thus by proof of Topology forms Complete Lattice:
- $x \subseteq \bigcup G$
$\Box$
Necessary Condition
Assume that
Let $I$ be an ideal in $\struct {\tau, \preceq}$ such that
- $y \preceq \sup I$
By proof of Topology forms Complete Lattice:
- $y \subseteq \bigcup I$
By assumption:
By proof of Topology forms Complete Lattice:
- $x \preceq \sup I$
By definition of ideal:
By Directed iff Finite Subsets have Upper Bounds:
- $\exists u \in I: u$ is upper bound for $G$
By definition of supremum:
- $\sup G \preceq u$
By definition of transitivity:
- $x \preceq u$
Thus by definition of lower section:
- $x \in I$
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
- $x \ll y$
$\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 WAYBEL_3:34
- Mizar article WAYBEL_3:35