English
The source of the composition of two fiberwise open partial homeomorphisms is the fiberwise product over the intersection of the base domains, i.e., the source becomes (U ∩ U') × universal fiber.
Русский
Область определения композиции двух открытых частичных гомоморфизмов вдоль волокон равна произведению по основанию: (U ∩ U') × универсуальная часть волокна.
LaTeX
$$$\\text{source}(\\text{openPartialHomeomorph }\\phi hU hφ h2φ \\;\\circ\\; \\text{openPartialHomeomorph }\\phi' hU' hφ' h2φ') = (U \\cap U') \\times \\univ$.$$
Lean4
/-- Compute the source of the composition of two open partial homeomorphisms induced by fiberwise
linear equivalences. -/
theorem source_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φ').source =
(U ∩ U') ×ˢ univ :=
by dsimp only [FiberwiseLinear.openPartialHomeomorph]; mfld_set_tac
