PartialHomeomorphHelpers

Supporting results for the classification of compact one-dimensional manifolds.

theorem OneMfld.partial_homeo_connected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : OpenPartialHomeomorph X Y) (conn : IsConnected h.source) : IsConnected h.target

theorem OneMfld.partial_homeo_connected' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : OpenPartialHomeomorph X Y) (conn : IsConnected h.target) : IsConnected h.source

theorem OneMfld.partial_homeo_source_connected_iff_target_connected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : OpenPartialHomeomorph X Y) : IsConnected h.source ↔ IsConnected h.target

theorem OneMfld.restrOpen_symm_image_target {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (φ : OpenPartialHomeomorph X Y) {t : Set Y} (ht : t ⊆ φ.target) : φ.target ∩ ↑φ.symm ⁻¹' ↑φ.symm '' t = t

For t ⊆ φ.target, the target of φ restricted to φ.symm '' t is exactly t; this computes (φ.restrOpen (φ.symm '' t) _).target.