FiberwiseLinear.target_trans_partialHomeomorph
theorem FiberwiseLinear.target_trans_partialHomeomorph :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U)
(hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U) (hU' : IsOpen U')
(hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'),
((FiberwiseLinear.partialHomeomorph φ hU hφ h2φ).trans
(FiberwiseLinear.partialHomeomorph φ' hU' hφ' h2φ')).target =
(U ∩ U') ×ˢ Set.univ
The theorem `FiberwiseLinear.target_trans_partialHomeomorph` states that for any two fiberwise linear equivalences `φ` and `φ'` (which are continuous functions mapping each point from a base space `B` to an isomorphic copy of a vector space `F`) defined on open sets `U` and `U'` respectively, the target of the composition of the two induced partial homeomorphisms is the cartesian product of the intersection of `U` and `U'` and the universal set. The continuity conditions required are that both `φ` and `φ'`, as well as their inverses, should be continuous on their respective domains. The base space `B` and the vector space `F` carry topologies, and `F` is a normed additive commutative group over a non-trivially normed field `𝕜`.
More concisely: Given fiberwise linear equivalences φ and φ' between open sets U and U' of a base space B with values in a normed vector space F, if both φ, φ', and their inverses are continuous, then the target of their composition is the intersection of U and U' in B, paired with any element in F.
|
FiberwiseLinear.source_trans_partialHomeomorph
theorem FiberwiseLinear.source_trans_partialHomeomorph :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U)
(hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U) (hU' : IsOpen U')
(hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'),
((FiberwiseLinear.partialHomeomorph φ hU hφ h2φ).trans
(FiberwiseLinear.partialHomeomorph φ' hU' hφ' h2φ')).source =
(U ∩ U') ×ˢ Set.univ
This theorem, "FiberwiseLinear.source_trans_partialHomeomorph", states that for any non-trivially normed field 𝕜, topological space B, and normed additive commutative group F, given two fiberwise linear equivalences φ and φ' from B to F, and two open sets U and U' in B, if both φ and its inverse are continuous on U, and both φ' and its inverse are continuous on U', then the source of the composition of the partial homeomorphisms induced by φ and φ', is equal to the cartesian product of the intersection of U and U' with the universal set. In other words, all points in the intersection of U and U' together with all possible points in the space form the source for the composite partial homeomorphism.
More concisely: Given two fiberwise linear equivalences between a topological space and a normed additive commutative group with continuous inverses on intersecting open sets, their composite partial homeomorphism has the intersection of those open sets as its source.
|