description/proof of that restriction of lower semicontinuous map on domain is lower semicontinuous
Topics
About: topological space
The table of contents of this article
Starting Context
Target Context
- The reader will have a description and a proof of the proposition that for any semicontinuous map, the restriction of the map on any domain is lower semicontinuous.
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 }\}\)
\(\overline{\mathbb{R}}\): \(= \text{ the extended Euclidean topological space }\)
\(f\): \(: T'_1 \to \overline{\mathbb{R}}\), \(\in \{\text{ the lower semicontinuous maps }\}\)
\(T_1\): \(\subseteq T'_1\), with the subspace topology
\(f \vert_{T_1}\): \(: T_1 \to \overline{\mathbb{R}}\)
//
Statements:
\(f \vert_{T_1} \in \{\text{ the lower semicontinuous maps }\}\)
//
2: Proof
Whole Strategy: Step 1: for each \(t_1 \in T_1\) and each \(r \lt f \vert_{T_1} (t_1)\), take an open neighborhood of \(t_1\), \(U'_{t_1} \subseteq T'_1\), such that \(r \lt f (U'_{t_1})\), and take \(U_{t_1} := U'_{t_1} \cap T_1\).
Step 1:
Let \(t_1 \in T_1\) be any.
Let \(r \in \mathbb{R}\) be any such that \(r \lt f \vert_{T_1} (t_1)\).
As \(r \lt f \vert_{T_1} (t_1) = f (t_1)\) and \(f\) is lower semicontinuous, there is an open neighborhood of \(t_1\), \(U'_{t_1} \subseteq T'_1\), such that \(r \lt f (U'_{t_1})\).
Let us take \(U_{t_1} := U'_{t_1} \cap T_1\), which is an open neighborhood of \(t_1\) on \(T_1\), by the definition of subspace topology.
\(f \vert_{T_1} (U_{t_1}) = f (U_{t_1}) \subseteq f (U'_{t_1})\), which implies that \(r \lt f \vert_{T_1} (U_{t_1})\).
So, \(f \vert_{T_1}\) is lower semicontinuous.
