The outer-overlap lemma

The structural heart of the classification: when two interval charts U, V overlap (neither source containing the other), the image under U of any connected component of U.source ∩ V.source is an end-segment of U.target — its closure reaches an open endpoint of the target. The mechanism: if the closure of the image stayed inside the target, the component's closure in M would be trapped inside U.source (a compactness argument), contradicting nonempty_closure_inter_diff, which forces the component's closure to escape into V.source \ U.source.

theorem OneMfld.OpenPartialHomeomorph.image_connectedComponentIn {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (φ : OpenPartialHomeomorph X Y) {S : Set X} (hS : S ⊆ φ.source) {x : X} (hx : x ∈ S) : ↑φ '' connectedComponentIn S x = connectedComponentIn (↑φ '' S) (↑φ x)

A partial homeomorphism maps the connected component of x in a subset S of its source onto the connected component of φ x in φ '' S.

theorem OneMfld.isOpen_connectedComponentIn_chart {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [LocallyConnectedSpace Y] (φ : OpenPartialHomeomorph X Y) {S : Set X} (hS : S ⊆ φ.source) (hSo : IsOpen S) (x : X) : IsOpen (connectedComponentIn S x)

Connected components of an open set contained in a chart source are open, because the model space is locally connected.

theorem OneMfld.mem_connectedComponentIn_of_mem_closure {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [LocallyConnectedSpace Y] (φ : OpenPartialHomeomorph X Y) {S : Set X} (hS : S ⊆ φ.source) (hSo : IsOpen S) {x z : X} (hz : z ∈ closure (connectedComponentIn S x)) (hzS : z ∈ S) : z ∈ connectedComponentIn S x

Components of an open set contained in a chart source are relatively closed: a point of S in the closure of a component of S lies in that component.

theorem OneMfld.image_component_ne_target {M : Type u_1} [TopologicalSpace M] (U V : OpenPartialHomeomorph M NNReal) (hUV : (U.source \ V.source).Nonempty) {x : M} : ↑U '' connectedComponentIn (U.source ∩ V.source) x ≠ U.target

The image under U of a component of the overlap is not all of U.target (because U.source is not contained in V.source).

theorem OneMfld.not_closure_image_subset_target {M : Type u_1} [TopologicalSpace M] [T2Space M] (U V : OpenPartialHomeomorph M NNReal) (hUb : Bornology.IsBounded U.target) (hV : IsConnected V.source) (hVU : (V.source \ U.source).Nonempty) {x : M} (hx : x ∈ U.source ∩ V.source) : ¬closure (↑U '' connectedComponentIn (U.source ∩ V.source) x) ⊆ U.target

The heart of the outer-overlap argument: the closure (in ℝ≥0) of the image of an overlap component cannot stay inside the (bounded) chart target. Otherwise the component's closure in M would be a subset of the compact set U.symm '' closure (U '' W) inside U.source — but by nonempty_closure_inter_diff the component's closure must reach a point of V.source outside the component, and any such point trapped in U.source ∩ V.source would belong to the component after all.

theorem OneMfld.eq_Ioo_of_closure_not_subset_Iio {v : NNReal} {A : Set NNReal} (hA : A ⊆ Set.Iio v) (hAo : IsOpen A) (hAc : IsConnected A) (hAne : A ≠ Set.Iio v) (hesc : ¬closure A ⊆ Set.Iio v) : ∃ p < v, A = Set.Ioo p v

A nonempty open connected subset of Iio v ⊆ ℝ≥0, other than Iio v itself, whose closure is not contained in Iio v, is an upper end-segment Ioo p v.

theorem OneMfld.eq_end_segment_of_closure_not_subset_Ioo {u v : NNReal} {A : Set NNReal} (hA : A ⊆ Set.Ioo u v) (hAo : IsOpen A) (hAc : IsConnected A) (hesc : ¬closure A ⊆ Set.Ioo u v) : (∃ (p : NNReal), u ≤ p ∧ p < v ∧ A = Set.Ioo p v) ∨ ∃ (q : NNReal), u < q ∧ q ≤ v ∧ A = Set.Ioo u q

A nonempty open connected subset of Ioo u v ⊆ ℝ≥0 whose closure is not contained in Ioo u v is an end-segment: Ioo p v or Ioo u q.

theorem OneMfld.overlap_component_outer_Iio {M : Type u_1} [TopologicalSpace M] [T2Space M] (U V : OpenPartialHomeomorph M NNReal) {v : NNReal} (hUt : U.target = Set.Iio v) (hV : IsConnected V.source) (hUV : (U.source \ V.source).Nonempty) (hVU : (V.source \ U.source).Nonempty) {x : M} (hx : x ∈ U.source ∩ V.source) : ∃ p < v, ↑U '' connectedComponentIn (U.source ∩ V.source) x = Set.Ioo p v

Outer-overlap lemma, boundary-chart case. If U has target Iio v and overlaps V (neither source containing the other), the image under U of any connected component of the overlap is an upper end-segment Ioo p v.

theorem OneMfld.overlap_component_outer_Ioo {M : Type u_1} [TopologicalSpace M] [T2Space M] (U V : OpenPartialHomeomorph M NNReal) {u v : NNReal} (hUt : U.target = Set.Ioo u v) (hV : IsConnected V.source) (hVU : (V.source \ U.source).Nonempty) {x : M} (hx : x ∈ U.source ∩ V.source) : (∃ (p : NNReal), u ≤ p ∧ p < v ∧ ↑U '' connectedComponentIn (U.source ∩ V.source) x = Set.Ioo p v) ∨ ∃ (q : NNReal), u < q ∧ q ≤ v ∧ ↑U '' connectedComponentIn (U.source ∩ V.source) x = Set.Ioo u q

Outer-overlap lemma, interior-chart case. If U has target Ioo u v and overlaps V, the image under U of any connected component of the overlap is an end-segment Ioo p v or Ioo u q.