Gluing two charts into an ℝ≥0-valued chart

The shared assembly for the O-H and O-O (connected overlap) cases. Chart a is normalized so its target is Ioo 0 1 and the overlap image is the full lower end-segment Ioo 0 r; chart b sees the overlap as an upper end-segment Ioo q 1 of its target. Pick a split value μ ∈ Ioo q 1, let m := b.symm μ be the split point and ρ := a m its a-coordinate; glue b (kept as-is on the b-side s, where b ≤ μ) with the rescaled chart (μ/ρ) • a (which agrees with b at m) using OpenPartialHomeomorph.piecewise along s := b.source ∩ b⁻¹' (Iic μ), t := Iic μ. All the frontier conditions come from IsImage.frontier and frontier_Iic.

theorem OneMfld.glue_nnreal {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) (hat : a.target = Set.Ioo 0 1) (hbt : b.target ⊆ Set.Iio 1) {r q : NNReal} (ha : ↑a '' (a.source ∩ b.source) = Set.Ioo 0 r) (hr0 : 0 < r) (hr1 : r < 1) (hb : ↑b '' (a.source ∩ b.source) = Set.Ioo q 1) (hq : q ∈ b.target) : ∃ (f : OpenPartialHomeomorph M NNReal), f.source = a.source ∪ b.source ∧ ∃ (μ : NNReal) (ρ : NNReal), q < μ ∧ μ < 1 ∧ 0 < ρ ∧ ρ < 1 ∧ f.target = b.target ∩ Set.Iic μ ∪ Set.Ioo μ (μ / ρ)

NNReal gluing. Given charts a (target Ioo 0 1, overlap image the lower end-segment Ioo 0 r) and b (target inside Iio 1, overlap image the upper end-segment Ioo q 1 with q interior), there is a chart on a.source ∪ b.source whose target is (b.target ∩ Iic μ) ∪ Ioo μ (μ/ρ) for some split values q < μ < 1, 0 < ρ < 1.