description/proof of that local homeomorphism is continuous
Topics
About: topological space
The table of contents of this article
Starting Context
- The reader knows a definition of local homeomorphism.
- The reader knows a definition of continuous, topological spaces map.
- The reader admits the proposition that for any topological space and any topological subspace that is open on the base space, any subset of the subspace is open on the subspace if and only if it is open on the base space.
Target Context
- The reader will have a description and a proof of the proposition that any local homeomorphism is continuous.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(T_1\): \(\in \{\text{ the topological spaces }\}\)
\(T_2\): \(\in \{\text{ the topological spaces }\}\)
\(f\): \(: T_1 \to T_2\), \(\in \{\text{ the local homeomorphisms }\}\)
//
Statements:
\(f \in \{\text{ the continuous maps }\}\)
//
2: Proof
Whole Strategy: Step 1: take any \(t \in T_1\) and any open neighborhood of \(f (t)\), \(U'_{f (t)}\); Step 2: take an open neighborhood of \(t\), \(U_t\), and an open neighborhood of \(f (t)\), \(U_{f (t)}\), such that \(f \vert_{U_t}: U_t \to U_{f (t)}\) is a homeomorphism; Step 3: see that \({f \vert_{U_t}}^{-1} (U'_{f (t)} \cap U_{f (t)})\) is an open neighborhood of \(t\) on \(T_1\) and \(f ({f \vert_{U_t}}^{-1} (U'_{f (t)} \cap U_{f (t)})) \subseteq U'_{f (t)}\).
Step 1:
Let \(t \in T_1\) be any.
Let \(U'_{f (t)} \subseteq T_2\) be any open neighborhood of \(f (t)\).
What we need to see is that there is an open neighborhood of \(t\) on \(T_1\) whose image under \(f\) is contained in \(U'_{f (t)}\).
Step 2:
There are an open neighborhood of \(t\), \(U_t \subseteq T_1\), and an open neighborhood of \(f (t)\), \(U_{f (t)} \subseteq T_2\), such that \(f \vert_{U_t}: U_t \to U_{f (t)}\) is a homeomorphism.
Step 3:
\(U'_{f (t)} \cap U_{f (t)} \subseteq U_{f (t)}\) is an open neighborhood of \(f (t)\) on \(U_{f (t)}\).
So, \({f \vert_{U_t}}^{-1} (U'_{f (t)} \cap U_{f (t)}) \subseteq U_t\) is an open neighborhood of \(t\) on \(U_t\), which is open on \(T_1\), by the proposition that for any topological space and any topological subspace that is open on the base space, any subset of the subspace is open on the subspace if and only if it is open on the base space.
\(f ({f \vert_{U_t}}^{-1} (U'_{f (t)} \cap U_{f (t)})) = f \vert_{U_t} ({f \vert_{U_t}}^{-1} (U'_{f (t)} \cap U_{f (t)})) = U'_{f (t)} \cap U_{f (t)} \subseteq U'_{f (t)}\).
