English
Given two trivializations e and e' and a set s with a compatibility condition on their base sets with frontier s, there is a new trivialization piecewise e e' s that agrees with e on proj^{-1}(s) and with e' elsewhere, with a specified base set and source/target behavior.
Русский
Для двух тривиализаций и множества s существует новая тривиализация piecewise, совпадающая с e на proj^{-1}(s) и с e' в противном случае, с заданными свойствами области определения и отображения.
LaTeX
$$$\\text{piecewise}(e,e',s,Hs,Heq)$$$
Lean4
/-- Given two bundle trivializations `e`, `e'` of `proj : Z → B` and a set `s : Set B` such that
the base sets of `e` and `e'` intersect `frontier s` on the same set and `e p = e' p` whenever
`proj p ∈ e.baseSet ∩ frontier s`, `e.piecewise e' s Hs Heq` is the bundle trivialization over
`Set.ite s e.baseSet e'.baseSet` that is equal to `e` on `proj ⁻¹ s` and is equal to `e'`
otherwise. -/
noncomputable def piecewise (e e' : Trivialization F proj) (s : Set B)
(Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s) (Heq : EqOn e e' <| proj ⁻¹' (e.baseSet ∩ frontier s)) :
Trivialization F proj
where
toOpenPartialHomeomorph :=
e.toOpenPartialHomeomorph.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) (e.isImage_preimage_prod s)
(e'.isImage_preimage_prod s) (by rw [e.frontier_preimage, e'.frontier_preimage, Hs])
(by rwa [e.frontier_preimage])
baseSet := s.ite e.baseSet e'.baseSet
open_baseSet := e.open_baseSet.ite e'.open_baseSet Hs
source_eq := by simp [source_eq]
target_eq := by simp [target_eq, prod_univ]
proj_toFun p := by rintro (⟨he, hs⟩ | ⟨he, hs⟩) <;> simp [*]
