ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4541 on D519: Set interior
Open set is its own interior
Formulation 0
Let $T = (X, \mathcal{T})$ be a D1106: Topological space such that
(i) $U \in \mathcal{T}$ is an D97: Open set in $T$
Then \begin{equation} \text{int} \langle U \rangle = U \end{equation}
Subresults
R1149: Every point in open set is an interior point
Proofs
Proof 0
Let $T = (X, \mathcal{T})$ be a D1106: Topological space such that
(i) $U \in \mathcal{T}$ is an D97: Open set in $T$
By definition \begin{equation} \text{int} \langle U \rangle : = \bigcup \{ V \in \mathcal{T} : V \subseteq U \} \end{equation} Result R125: Subset relation is reflexive shows that $U$ itself satisfies $U \subseteq U$. Since $U$ is also an open set, then $U$ is a set in the union $\text{int} \langle U \rangle$ and result R4142: Union is an upper bound to each set in the union implies that $U \subseteq \text{int} \langle U \rangle$.

Conversely, result R3945: Set is a superset to its interior guarantees that $\text{int} \langle U \rangle \subseteq U$. Since we have inclusions in both directions, the claim then follows as a consequence of R2741: Set equality iff inclusion in both directions. $\square$