Top in Ordered Set of Topology
Jump to navigation
Jump to search
Theorem
Let $T = \left({S, \tau}\right)$ be a topological space.
Let $P = \left({\tau, \subseteq}\right)$ be an inclusion ordered set of $\tau$.
Then $P$ is bounded above and $\top_P = S$
where $\top_P$ denotes the greatest element in $P$.
Proof
By definition of topological space:
- $S \in \tau$
By definition of subset:
- $\forall A \in \tau: A \subseteq S$
Hence $P$ is bounded above.
Thus by definition of the greatest element:
- $\top_P = S$
$\blacksquare$
Sources
- Mizar article YELLOR_1:24