English
In a setting with a linear order on the base, for a and e, e', He, He', and Heq, there is a piecewiseLeOfEq construction producing a trivialization that equals e on {proj p ≤ a} and equals e' elsewhere, subject to equality constraints on fibers.
Русский
При линейном порядке на основании строится piecewiseLeOfEq тривиализация, которая совпадает с e на ≤ a и с e' в противном случае при заданных условиях.
LaTeX
$$$\\text{piecewiseLeOfEq}(e,e',a)(He)(He')(Heq)$$$
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` such that
`e` equals `e'` on `proj ⁻¹' {a}`, `e.piecewise_le_of_eq e' a He He' Heq` 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'` otherwise. -/
noncomputable def piecewiseLeOfEq [LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj) (a : B)
(He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) (Heq : ∀ p, proj p = a → e p = e' p) : Trivialization F proj :=
e.piecewise e' (Iic a)
(Set.ext fun x =>
and_congr_left_iff.2 fun hx =>
by
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)
simp [He, He'])
fun p hp => Heq p <| frontier_Iic_subset _ hp.2
