English
The target of the composition of two fiberwise open partial homeomorphisms is the intersection domain with universal fiber, i.e., (U ∩ U') × univ.
Русский
Целью композиции является пересечение базисных областей вдоль волокна с полной пространственной частью: (U ∩ U') × univ.
LaTeX
$$$\\text{target}(\\text{openPartialHomeomorph }\\phi hU hφ h2φ \\;≫\\; \\text{openPartialHomeomorph }\\phi' hU' hφ' h2φ') = (U \\cap U') \\times \\univ$.$$
Lean4
/-- Compute the target of the composition of two open partial homeomorphisms induced by fiberwise
linear equivalences. -/
theorem target_trans_openPartialHomeomorph (hU : IsOpen U) (hφ : ContinuousOn (fun x => φ x : B → F →L[𝕜] F) U)
(h2φ : ContinuousOn (fun x => (φ x).symm : B → F →L[𝕜] F) U) (hU' : IsOpen U')
(hφ' : ContinuousOn (fun x => φ' x : B → F →L[𝕜] F) U')
(h2φ' : ContinuousOn (fun x => (φ' x).symm : B → F →L[𝕜] F) U') :
(FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ ≫ₕ
FiberwiseLinear.openPartialHomeomorph φ' hU' hφ' h2φ').target =
(U ∩ U') ×ˢ univ :=
by dsimp only [FiberwiseLinear.openPartialHomeomorph]; mfld_set_tac
