English
Let e and e' be trivializations of a fibre bundle over a linearly ordered base B, and let a be a point in e.baseSet ∩ e'.baseSet. Then there exists a trivialization e_piecesle e' that is defined on the set where proj(p) ≤ a by agreeing with e, and on the other part by using the fiber coordinate change from e' to align with e at a. This new trivialization uses the homeomorphism h = e'.coord_change_homeomorph e He' He to rotate the fibre appropriately.
Русский
Пусть e и e' – тривиализации расслоения фибры над базой B, линейно упорядоченной, и возьмём a ∈ e.baseSet ∩ e'.baseSet. Тогда существует локальная триивиализация e_piecesLe e', определяемая на множествах Set.ite(Iic a) ∪ ... так, чтобы на точках p с proj p ≤ a она совпадала с e, а в противном случае применяла координатное преобразование h = e'.coordChangeHomeomorph e He' He к элементу фибры, чтобы согласовать с e на a.
LaTeX
$$$\text{piecewiseLe}(e,e',a,He,He')$ is a Trivialization F proj over $Set.ite(Iic(a), e.baseSet, e'.baseSet)$ such that $\forall p,\;\text{proj}(p)\le a \Rightarrow \text{(piecewiseLe)}(p)=e(p)$ and $\text{otherwise}\;\text{(piecewiseLe)}(p)= ((e'p).1, h (e'p).2)$ with $h=e'.coordChangeHomeomorph e He' He$.$$
Lean4
/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B` over a
linearly ordered base `B` and a point `a ∈ e.baseSet ∩ e'.baseSet`, `e.piecewise_le e' a He He'`
is the bundle trivialization over `Set.ite (Iic a) e.baseSet e'.baseSet` that is equal to `e` on
points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
`h = e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
`h (e' p).2 = (e p).2` whenever `e p = a`. -/
noncomputable def piecewiseLe [LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj) (a : B)
(He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) : Trivialization F proj :=
e.piecewiseLeOfEq (e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) a He He' <|
by
rintro p rfl
ext1
· simp [e.coe_fst', e'.coe_fst', *]
· simp [coordChange_apply_snd, *]
