<The previous article in this series | The table of contents of this series |
description/proof of that finite product of open maps is open
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 any finite product of open maps is open.
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 finite index sets }\}\)
\(\{T_{1, j} \vert j \in J\}\): \(T_{1, j} \in \{\text{ the topological spaces }\}\)
\(\{T_{2, j} \vert j \in J\}\): \(T_{2, j} \in \{\text{ the topological spaces }\}\)
\(\{f_j \vert j \in J\}\): \(f_j: T_{1, j} \to T_{2, j} \in \{\text{ the open maps }\}\)
//
Statements:
\(\times_{j \in J} f_j \in \{\text{ the open maps }\}\)
//
2: Note
This proposition requires that \(J\) is finite, because of the reason mentioned in Proof.
3: Proof
Whole Strategy: Step 1: take any open subset, \(U \subseteq \times_{j \in J} T_{1, j}\), and see that \(U = \cup_{j' \in J'} \times_{j \in J} U_{1, j, j'}\); Step 2: see that \((\times_{j \in J} f_j) (U) = \cup_{j' \in J'} \times_{j \in J} f_j (U_{1, j, j'})\).
Step 1:
Let \(U \subseteq \times_{j \in J} T_{1, j}\) be any open subset.
\(U = \cup_{j' \in J'} \times_{j \in J} U_{1, j, j'}\) where \(J'\) is a possibly uncountable index set and \(U_{1, j, j'} \subseteq T_{1, j} \) is open: refer to Note for the definition of product topology.
Step 2:
\((\times_{j \in J} f_j) (U) = (\times_{j \in J} f_j) (\cup_{j' \in J'} \times_{j \in J} U_{1, j, j'}) = \cup_{j' \in J'} (\times_{j \in J} f_j) (\times_{j \in J} U_{1, j, j'})\), by the proposition that for any map, the map image of any union of sets is the union of the map images of the sets, \(= \cup_{j' \in J'} \times_{j \in J} f_j (U_{1, j, j'})\), by the proposition that for any product map, the image of any product subset is the product of the images of the component subsets under the component maps.
As each \(f_j\) is open, each \(f_j (U_{1, j, j'}) \subseteq T_{2, j}\) is open.
So, \(\cup_{j' \in J'} \times_{j \in J} f_j (U_{1, j, j'})\) is open: refer to Note for the definition of product topology.
Note that this proposition requires \(J\) to be finite, because otherwise, for each fixed \(j'\), while only finite of \(f_j (U_{1, j, j'})\) s were allowed to be not \(T_{2, j}\), which would not be guaranteed: the fact that only finite of \(U_{1, j, j'}\) s were not \(T_{1, j}\) would not guaranteed the requirement, because \(f_j\) s were not necessarily surjective.
So, \(\times_{j \in J} f_j\) is open.
References
<The previous article in this series | The table of contents of this series |
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for product map, image of product subset is product of images of component subsets under component maps
Topics
About:
set
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 product map, the image of any product subset is the product of the images of the component subsets under the component maps.
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 }\}\)
\(\{S_{1, j} \vert j \in J\}\): \(S_{1, j} \in \{\text{ the sets }\}\)
\(\{S_{2, j} \vert j \in J\}\): \(S_{2, j} \in \{\text{ the sets }\}\)
\(\{f_j \vert j \in J\}\): \(f_j: S_{1, j} \to S_{2, j}\)
\(\{S^`_{1, j} \vert j \in J\}\): \(S^`_{1, j} \subseteq S_{1, j}\)
//
Statements:
\((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\)
//
2: Note
In the definition of product map, the product map by Description 1 and the product map by Description 2 are not exactly the same, but as the logics of Proof for the 2 definitions are basically the same, Proof does not distinguish them.
As a notation, for any \(s \in \times_{j \in J} S_{l, j}\), \(s^m\) denotes the \(m\)-component of \(s\).
3: Proof
Whole Strategy: Step 1: see that \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\); Step 2: see that \(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\); Step 3: conclude the proposition.
Step 1:
Let \(s \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\) be any.
There is an \(s' \in \times_{j \in J} S^`_{1, j}\) such that \(s = (\times_{j \in J} f_j) (s')\).
\(s' \in \times_{j \in J} S^`_{1, j}\) means that \(s'^j \in S^`_{1, j}\), so, \(f_j (s'^j) \in f_j (S^`_{1, j})\).
\(s = (\times_{j \in J} f_j) (s') = \times_{j \in J} f_j (s'^j) \subseteq \times_{j \in J} f_j (S^`_{1, j})\).
So, \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\).
Step 2:
Let \(s \in \times_{j \in J} f_j (S^`_{1, j})\) be any.
\(s^j \in f_j (S^`_{1, j})\).
There is an \(s'^j \in S^`_{1, j}\) such that \(s^j = f_j (s'^j)\).
\(\times_{j \in J} s'^j \in \times_{j \in J} S^`_{1, j}\).
\(s = \times_{j \in J} s^j = (\times_{j \in J} f_j) (\times_{j \in J} s'^j) \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\).
So, \(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\).
Step 3:
So, \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that \(C^\infty\) local section of \(C^\infty\) vectors bundle is \(C^\infty\) embedding
Topics
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that any \(C^\infty\) local section of any \(C^\infty\) vectors bundle is a \(C^\infty\) embedding.
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:
\(k\): \(\in \mathbb{N} \setminus \{0\}\)
\((E, M, \pi)\): \(\in \{\text{ the } C^\infty \text{ vectors bundles of rank } k\}\)
\(U\): \(\in \{\text{ the open embedded submanifolds with boundary of } M\}\)
\(s\): \(: U \to E\), \(\in \{\text{ the } C^\infty \text{ local sections of } \pi\}\)
//
Statements:
\(s \in \{\text{ the } C^\infty \text{ embeddings }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \(s\) is a \(C^\infty\) injective immersion; Step 2: see that the codomain restriction of \(s\) is a homeomorphism; Step 3: conclude the proposition.
Step 1:
\(s\) is an injection, because for each \(u_1, u_2 \in U\) such that \(u_1 \neq u_2\), \(s (u_1) \neq s (u_2)\), because if \(s (u_1) = s (u_2)\), \(u_1 = \pi \circ s (u_1) = \pi \circ s (u_2) = u_2\), a contradiction against \(u_1 \neq u_2\).
Let us see that \(s\) is a \(C^\infty\) immersion.
\(s\) is \(C^\infty\), by the supposition.
Let \(u \in U\) be any.
Let us take any trivializing chart, \((U_u \subseteq U, \phi_u)\), with a trivialization, \(\Phi: \pi^{-1} (U_u) \to U_u \times \mathbb{R}^k\), by the proposition that for any \(C^\infty\) vectors bundle, a trivializing open subset is not necessarily a chart open subset, but there is a possibly smaller chart trivializing open subset at each point on any trivializing open subset: take a trivializing open neighborhood of \(u\), \(U'_u \subseteq M\), such that \(U'_u \subseteq U\), and take \(U_u\) such that \(U_u \subseteq U'_u\).
By the proposition that for any \(C^\infty\) vectors bundle, the trivialization of any chart trivializing open subset induces the canonical chart map, there is the canonical chart, \((\pi^{-1} (U_u) \subseteq E, \widetilde{\phi_u})\), where \(\widetilde{\phi_u}: \pi^{-1} (U_u) \to U_u \times \mathbb{R}^k \to \mathbb{R}^{d + k} \text{ or } \mathbb{H}^{d + k}, v \mapsto (\pi_2 (\Phi (v)), \phi_u (\pi (v)))\), where \(\pi_2: U_u \times \mathbb{R}^k \to \mathbb{R}^k\) is the projection.
Let us think of the differential of \(s\) at \(u\), \(d s_u: T_uU \to T_{s (u)}E\).
With the standard bases for \(T_uU\) and \(T_{s (u)}E\) with respect to the charts, the components function of \(d s_u\) is \((v^j) \mapsto (\partial_l \hat{s}^j v^l)\) where \(\hat{s} = \widetilde{\phi_u} \circ s \circ {\phi_u}^{-1}: \phi_u (U_u) \subseteq \mathbb{R}^d \to \widetilde{\phi_u} (\pi^{-1} (U_u)) \subseteq \mathbb{R}^{d + k} \text{ or } \mathbb{H}^{d + k}\) is the components function of \(s\), by the proposition that for any \(C^\infty\) map between any \(C^\infty\) manifolds with boundary and any corresponding charts, the components function of the differential of the map with respect to the standard bases is this.
For each \(j \in \{k + 1, ..., k + d\}\), \(\hat{s}^j: (x^1, ..., x^d) \mapsto x^{j - k}\), so, \(\partial_l \hat{s}^j = \delta^{j - k}_l\), so, \(\partial_l \hat{s}^j v^l = \delta^{j - k}_l v^l = v^{j - k}\).
So, for each \(v, v' \in T_uU\) such that \(v \neq v'\), \(v^l \neq v'^l\) for an \(l \in \{1, ..., d\}\), so, \(\partial_l \hat{s}^j v^l = v^{j - k} \neq v'^{j - k} = \partial_l \hat{s}^j v'^l\) for \(j = l + k\).
So, \(d s_u (v) \neq d s_u (v')\).
So, \(d s_u\) is injective, so, \(s\) is a \(C^\infty\) immersion.
Step 2:
Let us see that the codomain restriction of \(s\), \(s': U \to s (U)\), is a homeomorphism.
\(s\) is continuous, because \(s\) is \(C^\infty\), and \(s'\) is continuous, by the proposition that any restriction of any continuous map on the domain and the codomain is continuous.
As \(s\) is injective, there is the inverse, \(s'^{-1}: s (U) \to U\).
\(s'^{-1}\) is nothing but the restriction of \(\pi\), \(\pi \vert_{s (U)}: s (U) \to U\).
\(\pi\) is continuous, and \(\pi \vert_{s (U)}\) is continuous, by the proposition that any restriction of any continuous map on the domain and the codomain is continuous.
So, \(s'^{-1}\) is continuous.
So, \(s'\) is a homeomorphism.
Step 3:
So, \(s\) is a \(C^\infty\) embedding.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for finite-dimensional vectors space with inner product with induced topology, map from space into space is unitary iff map is represented by unitary matrix w.r.t. orthonormal basis
The table of contents of this article
Main Body
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for map from module with \(d_1\)-elements basis into module with \(d_2\)-elements basis over same ring, map is linear iff map is represented by \(d_2 \times d_1\) ring matrix
Topics
About:
module
About:
matrices 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 map from any module with any \(d_1\)-elements basis into any module with any \(d_2\)-elements basis over any same ring, the map is linear if and only if the map is represented by the \(d_2 \times d_1\) ring matrix.
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:
\(R\): \(\in \{\text{ the rings }\}\)
\(M_1\): \(\in \{\text{ the } R \text{ modules }\}\), with any basis, \(B_1 = \{b_{1, 1}, ..., b_{1, d_1}\}\)
\(M_2\): \(\in \{\text{ the } R \text{ modules }\}\), with any basis, \(B_2 = \{b_{2, 1}, ..., b_{2, d_2}\}\)
\(f\): \(: M_1 \to M_2\)
\(M\): \(\in \{\text{ the } d_2 \times d_1 R \text{ matrices }\}\), such that \(f (b_{1, j}) = M^l_j b_{2, l}\)
//
Statements:
\(f \in \{\text{ the linear maps }\}\)
\(\implies\)
\(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\)
//
2: Note
\(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\) means nothing but "\(f\) is represented by \(M\)", because \(M\) determines \(f\), because the decomposition, \(v^j b_{1, j}\), is unique, by the proposition that for any module with any basis, the components set of any element with respect to the basis is unique.
When \(R\) is commutative, it means that \(\begin{pmatrix} {v_2}^1 \\ ... \\ {v_2}^{d_2} \end{pmatrix} = M \begin{pmatrix} {v_1}^1 \\ ... \\ {v_1}^{d_1} \end{pmatrix}\) where \(v_2 := f (v_1) = {v_2}^l b_{2, l}\); when \(R\) is not commutative, \({v_1}^j M^l_j b_{2, l}\) cannot be expressed so, because \({v_1}^j M^l_j \neq M^l_j {v_1}^j\) in general while \(M \begin{pmatrix} {v_1}^1 \\ ... \\ {v_1}^{d_1} \end{pmatrix}\) produces the latter.
3: Proof
Whole Strategy: Step 1: see that \(M\) is well-defined and \({v_1}^j M^l_j b_{2, l}\) is uniquely determined; Step 2: suppose that \(f\) is linear; Step 3: see that \(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\); Step 4: suppose that \(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\); Step 5: see that \(f\) is linear.
Step 1:
Let us see that \(M\) is well-defined.
\(M\) is uniquely determined, by the proposition that for any module with any basis, the components set of any element with respect to the basis is unique: \(M^l_j b_{2, l}\) is the decomposition of \(f (b_{1, j})\) with respect to \(B_2\) where \(M^l_j \in R\).
\(M\) is indeed a \(d_2 \times d_1\) \(R\) matrix, because \(l \in \{1, ..., d_2\}\) and \(j \in \{1, ..., d_1\}\): when an \(l\) does not appear in \(M^l_j b_{2, l}\), \(M^l_j := 0\).
The decomposition, \(v_1 = {v_1}^j b_{1, j}\), is unique, by the proposition that for any module with any basis, the components set of any element with respect to the basis is unique: when a \(j\) does not appear in \({v_1}^j b_{1, j}\), \({v_1}^j := 0\).
So, \({v_1}^j M^l_j b_{2, l}\) is uniquely determined.
Step 2:
Let us suppose that \(f\) is linear.
Step 3:
Let us see that \(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\).
\(f (v_1) = f ({v_1}^j b_{1, j}) = {v_1}^j f (b_{1, j})\), because \(f\) is linear, \(= {v_1}^j M^l_j b_{2, l}\).
Step 4:
Let us suppose that \(\forall v_1 = {v_1}^j b_{1, j} \in M_1 (f (v_1) = {v_1}^j M^l_j b_{2, l})\).
Let \(v_1 = {v_1}^j b_{1, j}, v'_1 = {v'_1}^j b_{1, j} \in M_1\) and \(r, r' \in R\) be any.
\(f (r v_1 + r' v'_1) = f (r {v_1}^j b_{1, j} + r' {v'_1}^j b_{1, j}) = f ((r {v_1}^j + r' {v'_1}^j) b_{1, j}) = (r {v_1}^j + r' {v'_1}^j) M^l_j b_{2, l} = r ({v_1}^j M^l_j b_{2, l}) + r' ({v'_1}^j M^l_j b_{2, l}) = r f (v_1) + r' f (v'_1)\), which means that \(f\) is linear.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for finite-dimensional vectors space with inner product, components matrix of inner product w.r.t. basis is invertible
The table of contents of this article
Main Body
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that inverse of unitary matrix is unitary
Topics
About:
matrices 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 the inverse of any unitary matrix is unitary.
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:
\(M\): \(\in \{\text{ the unitary matrices }\}\)
\(M^{-1}\): \(= \text{ the inverse of } M\)
//
Statements:
\(M^{-1} \in \{\text{ the unitary matrices }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \(M^{-1} = M^*\); Step 2: apply the proposition that the Hermitian conjugate of any unitary matrix is unitary.
Step 1:
\(M^{-1} = M^*\), by the definition of unitary matrix.
Step 2:
\(M^*\) is unitary, by the proposition that the Hermitian conjugate of any unitary matrix is unitary, so, \(M^{-1}\) is unitary.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that Hermitian conjugate of unitary matrix is unitary
Topics
About:
matrices 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 the Hermitian conjugate of any unitary matrix is unitary.
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:
\(M\): \(\in \{\text{ the unitary matrices }\}\)
\(M^*\): \(= \text{ the Hermitian conjugate of } M\)
//
Statements:
\(M^* \in \{\text{ the unitary matrices }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \({M^*}^* = M\); Step 2: see that \({M^*}^* = {M^*}^{-1}\).
Step 1:
\({M^*}^* = M\), by the proposition that the Hermitian conjugate of the Hermitian conjugate of any complex matrix is the matrix.
Step 2:
\({M^*}^* M^* = M M^* = I\), because \(M\) is unitary.
\(M^* {M^*}^* = M^* M = I\), because \(M\) is unitary.
So, \({M^*}^* = {M^*}^{-1}\).
So, \(M^*\) is unitary.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that Hermitian conjugate of Hermitian conjugate of complex matrix is matrix
Topics
About:
matrices 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 the Hermitian conjugate of the Hermitian conjugate of any complex matrix is the matrix.
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:
\(M\): \(\in \{\text{ the } m \times n \text{ complex matrices }\}\)
\({M^*}^*\): \(= \text{ the Hermitian conjugate of the Hermitian conjugate of } M\)
//
Statements:
\({M^*}^* = M\)
//
2: Proof
Whole Strategy: Step 1: see that \({M^*}^*\) is an \(m \times n\) matrix; Step 2: see that \({{M^*}^*}^j_l = M^j_l\).
Step 1:
\(M^*\) is an \(n \times m\) matrix.
\({M^*}^*\) is an \(m \times n\) matrix.
Step 2:
\({{M^*}^*}^j_l = \overline{{M^*}^l_j} = \overline{\overline{M^j_l}} = M^j_l\).
So, \({M^*}^* = M\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for map between sets, image of intersection of preimages of codomain subsets is intersection of images of preimages of codomain subsets
Topics
About:
set
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 map between any sets, the image of the intersection of the preimages of any codomain subsets is the intersection of the images of the preimages of the codomain subsets.
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:
\(S_1\): \(\in \{\text{ the sets }\}\)
\(S_2\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S_1 \to S_2\)
\(J\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_{2, j} \subseteq S_2 \vert j \in J\}\):
//
Statements:
\(f (\cap_{j \in J} f^{-1} (S_{2, j})) = \cap_{j \in J} f (f^{-1} (S_{2, j}))\)
//
2: Proof
Whole Strategy: Step 1: see that \(f (\cap_{j \in J} f^{-1} (S_{2, j})) \subseteq \cap_{j \in J} f (f^{-1} (S_{2, j}))\); Step 2: see that \(\cap_{j \in J} f (f^{-1} (S_{2, j})) \subseteq f (\cap_{j \in J} f^{-1} (S_{2, j}))\); Step 3: conclude the proposition.
Step 1:
Let \(s \in f (\cap_{j \in J} f^{-1} (S_{2, j}))\) be any.
There is an \(s' \in \cap_{j \in J} f^{-1} (S_{2, j})\) such that \(f (s') = s\).
\(s' \in f^{-1} (S_{2, j})\) for each \(j \in J\).
\(s = f (s') \in f (f^{-1} (S_{2, j}))\) for each \(j\).
So, \(s \in \cap_{j \in J} f (f^{-1} (S_{2, j}))\).
So, \(f (\cap_{j \in J} f^{-1} (S_{2, j})) \subseteq \cap_{j \in J} f (f^{-1} (S_{2, j}))\).
Step 2:
Let \(s \in \cap_{j \in J} f (f^{-1} (S_{2, j}))\) be any.
\(s \in f (f^{-1} (S_{2, j}))\) for each \(j \in J\).
Let \(l \in J\) be any fixed one.
As \(s \in f (f^{-1} (S_{2, l}))\), there is an \(s' \in f^{-1} (S_{2, l})\) such that \(f (s') = s\).
Let \(m \in J\) be any.
\(s = f (s') \in f (f^{-1} (S_{2, m}))\).
So, \(s' \in f^{-1} (f (f^{-1} (S_{2, m})))\).
But \(f (f^{-1} (S_{2, m})) \subseteq S_{2, m}\).
So, \(f^{-1} (f (f^{-1} (S_{2, m}))) \subseteq f^{-1} (S_{2, m})\).
\(s' \in f^{-1} (f (f^{-1} (S_{2, m}))) \subseteq f^{-1} (S_{2, m})\).
So, \(s' \in \cap_{j \in J} f^{-1} (S_{2, j})\).
So, \(s = f (s') \in f (\cap_{j \in J} f^{-1} (S_{2, j}))\).
So, \(\cap_{j \in J} f (f^{-1} (S_{2, j})) \subseteq f (\cap_{j \in J} f^{-1} (S_{2, j}))\).
Step 3:
So, \(f (\cap_{j \in J} f^{-1} (S_{2, j})) = \cap_{j \in J} f (f^{-1} (S_{2, j}))\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for map between sets, image of preimage of codomain subset is intersection of codomain subset and map range
Topics
About:
set
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 map between any sets, the image of the preimage of any codomain subset is the intersection of the codomain subset and the map range.
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:
\(S_1\): \(\in \{\text{ the sets }\}\)
\(S_2\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S_1 \to S_2\)
\(S^`_2\): \(\subset S_2\)
//
Statements:
\(f (f^{-1} (S^`_2)) = S^`_2 \cap f (S_1)\)
//
2: Proof
Whole Strategy: Step 1: apply the proposition that for any map between any sets, the image of the intersection of the intersection of the preimages of any codomain subsets and any domain subset is the intersection of the intersection of the codomain subsets and the image of the domain subset.
Step 1:
For the proposition that for any map between any sets, the image of the intersection of the intersection of the preimages of any codomain subsets and any domain subset is the intersection of the intersection of the codomain subsets and the image of the domain subset, \(\cap_{j \in J} f^{-1} (S_{2, j})\) can be taken to be \(f^{-1} (S^`_2)\) and the domain subset can be taken to be \(S_1\), then \(f (f^{-1} (S^`_2) \cap S_1) = S^`_2 \cap f (S_1)\), but \(f (f^{-1} (S^`_2) \cap S_1) = f (f^{-1} (S^`_2))\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
