description/proof of that for lower semicontinuous map from subspace of product topological space into \(1\)-dimensional extended Euclidean topological space and element of subproduct, cross section of map is lower semicontinuous
Topics
About: topological space
The table of contents of this article
Starting Context
- The reader knows a definition of product topological space.
- The reader knows a definition of lower semicontinuous map from topological space into \(1\)-dimensional extended Euclidean topological space.
- The reader knows a definition of cross section of map from subset of product set by element of subproduct set.
- The reader admits the proposition that for any product topological space, any subspace, any open subset of the subspace, and any element of any subproduct, the cross section of the open subset by the element is open on the cross section of the subspace by the element.
Target Context
- The reader will have a description and a proof of the proposition that for any lower semicontinuous map from any subspace of any product topological space into the \(1\)-dimensional extended Euclidean topological space and any element of any subproduct, the cross section of the map by the element 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:
\(J'\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{T_{j'} \in \{\text{ the topological spaces }\} \vert j' \in J'\}\):
\(\times_{j' \in J'} T_{j'}\): \(= \text{ the product topological space }\)
\(T\): \(\subseteq \times_{j' \in J'} T_{j'}\), with the subspace topology
\(\overline{\mathbb{R}}\): \(= \text{ the extended Euclidean topological space }\)
\(f\): \(: T \to \overline{\mathbb{R}}\)
\(J\): \(\subset J'\), such that \(J \neq \emptyset\)
\(\times_{j \in J} t_j\): \(\in \times_{j \in J} T_j\)
\(f_{[\times_{j \in J} t_j]}\): \(: T_{[\times_{j \in J} t_j]} \to \overline{\mathbb{R}}\), \(= \text{ the cross section }\)
//
Statements:
\(f \in \{\text{ the lower semicontinuous maps }\}\)
\(\implies\)
\(f_{[\times_{j \in J} t_j]} \in \{\text{ the lower semicontinuous maps }\}\)
//
2: Proof
Whole Strategy: Step 1: for each \(\times_{l \in J' \setminus J} t_l \in T_{[\times_{j \in J} t_j]}\) and each \(r \lt f_{[\times_{j \in J} t_j]} (\times_{l \in J' \setminus J} t_l)\), take a \(U_{\times_{j' \in J'} t_{j'}}\) such that \(r \lt f (U_{\times_{j' \in J'} t_{j'}})\), and see that \((U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\) is an open neighborhood of \(\times_{l \in J' \setminus J} t_l\) and \(r \lt f_{[\times_{j \in J} t_j]} ((U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]})\).
Step 1:
Let \(\times_{l \in J' \setminus J} t_l \in T_{[\times_{j \in J} t_j]}\) be any.
Let \(r \in \mathbb{R}\) be any such that \(r \lt f_{[\times_{j \in J} t_j]} (\times_{l \in J' \setminus J} t_l)\).
\(f_{[\times_{j \in J} t_j]} (\times_{l \in J' \setminus J} t_l) = f (\times_{j' \in J'} t_{j'})\).
As \(r \lt f (\times_{j' \in J'} t_{j'})\) and \(f\) is lower semicontinuous, there is an open neighborhood of \(\times_{j' \in J'} t_{j'}\), \(U_{\times_{j' \in J'} t_{j'}} \subseteq T\), such that \(r \lt f (U_{\times_{j' \in J'} t_{j'}})\).
\((U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\), the cross section of \(U_{\times_{j' \in J'} t_{j'}}\) by \(\times_{j \in J} t_j\), is an open neighborhood of \(\times_{l \in J' \setminus J} t_l\) on \(T_{[\times_{j \in J} t_j]}\), because \(\times_{j' \in J'} t_{j'} \in U_{\times_{j' \in J'} t_{j'}}\) and \((U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]} \subseteq T_{[\times_{j \in J} t_j]}\) is open, by the proposition that for any product topological space, any subspace, any open subset of the subspace, and any element of any subproduct, the cross section of the open subset by the element is open on the cross section of the subspace by the element.
Then, for each \(\times_{l \in J' \setminus J} u_l \in (U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]}\), taking for each \(j \in J\), \(u_j := t_j\), \(\times_{j' \in J'} u_l \in U_{\times_{j' \in J'} t_{j'}}\), so, \(f_{[\times_{j \in J} t_j]} (\times_{l \in J' \setminus J} u_l) = f (\times_{j' \in J'} u_l) \in f (U_{\times_{j' \in J'} t_{j'}})\), so, \(r \lt f_{[\times_{j \in J} t_j]} (\times_{l \in J' \setminus J} u_l)\), so, \(r \lt f_{[\times_{j \in J} t_j]} ((U_{\times_{j' \in J'} t_{j'}})_{[\times_{j \in J} t_j]})\).
So, \(f_{[\times_{j \in J} t_j]}\) is lower semicontinuous.
