Gluing two boundary charts onto the unit interval

The H-H assembly. Both charts are normalized to target Iio 1; each sees the overlap as an upper end-segment (Ioo p 1 in a, Ioo q 1 in b), and the transition is decreasing (overlap_anti). Embed b into the lower half of the unit interval via halfOPH (x ↦ x/2) and a into the upper piece via a decreasing Möbius map mobiusOPH k (x ↦ k/(x+k)), with k chosen so the two embeddings agree at the split point m := b.symm μ (that is, k/(ρ+k) = μ/2 where ρ := a m). Glue with OpenPartialHomeomorph.piecewise along t := {y ≤ μ/2}; the two targets [0, μ/2] and (μ/2, 1] unite to the whole interval.

theorem OneMfld.glue_hh_ui {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) (hat : a.target = Set.Iio 1) (hbt : b.target = Set.Iio 1) {p q : NNReal} (ha : ↑a '' (a.source ∩ b.source) = Set.Ioo p 1) (hp : p < 1) (hb : ↑b '' (a.source ∩ b.source) = Set.Ioo q 1) : ∃ (f : OpenPartialHomeomorph M ↑UnitInterval), f.source = a.source ∪ b.source ∧ f.target = Set.univ

Unit-interval gluing. Two boundary charts (targets Iio 1) whose overlap is an upper end-segment in each glue to a chart of M onto the whole unit interval, with source a.source ∪ b.source.