English
The composition of two fiberwise open partial homeomorphisms corresponds to fiberwise composition of their linear parts: composing two such fiberwise maps results in a new fiberwise linear open partial homeomorphism whose fiberwise action is the composition of the two linear isomorphisms at each base point.
Русский
Суммирование двух открытых частичных гомоморфизмов вдоль волокон соответствует по каждому базисному пункту композиции линейных отображений; получаем новый открытый частичный гомоморфизм вдоль волокон.
LaTeX
$$$\\big(\\text{openPartialHomeomorph } \\phi \\big) \\circ \\big(\\text{openPartialHomeomorph } \\psi \\big) = \\text{openPartialHomeomorph } (\\psi \\,\\circ\\, \\phi)$ на соответствующем домене, с действием по волокнам $v \\mapsto \\psi(b)(\\phi(b)(v))$.$$
Lean4
/-- Compute the composition of two open partial homeomorphisms induced by fiberwise linear
equivalences. -/
theorem trans_openPartialHomeomorph_apply (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') (b : B) (v : F) :
(FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ ≫ₕ FiberwiseLinear.openPartialHomeomorph φ' hU' hφ' h2φ')
⟨b, v⟩ =
⟨b, φ' b (φ b v)⟩ :=
rfl
