Closed Subset is Upper Section in Lower Topology
Jump to navigation
Jump to search
Theorem
Let $T = \struct {S, \preceq, \tau}$ be a transitive relational structure with lower topology.
Let $A \subseteq S$ such that
- $A$ is closed.
Then $A$ is an upper section of $S$.
Proof
By definition of closed set:
- $S \setminus A$ is open.
By Open Subset is Lower Section in Lower Topology:
- $S \setminus A$ is a lower section.
Thus by Complement of Lower Section is Upper Section and Relative Complement of Relative Complement:
- $A$ is an upper section of $S$.
$\blacksquare$
Sources
- Mizar article WAYBEL19:6