Partial homeomorphisms and continuity

Main theorems

• OpenPartialHomeomorph.map_nhds_eq: an open partial homeomorphism preserves the neighbourhood filter of any point in its source.
• OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left, OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right: a function is continuous at a point iff its pre / post composition with an open partial homeomorphism is so (assuming the point is in the source / target).

theorem OpenPartialHomeomorph.eventually_left_inverse {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y

theorem OpenPartialHomeomorph.eventually_left_inverse' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : X) in nhds (↑e.symm x), ↑e.symm (↑e y) = y

theorem OpenPartialHomeomorph.eventually_right_inverse {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y

theorem OpenPartialHomeomorph.eventually_right_inverse' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : Y) in nhds (↑e x), ↑e (↑e.symm y) = y

theorem OpenPartialHomeomorph.eventually_ne_nhdsWithin {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (x' : X) in nhdsWithin x {x}ᶜ, ↑e x' ≠ ↑e x

theorem OpenPartialHomeomorph.nhdsWithin_source_inter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set X) : nhdsWithin x (e.source ∩ s) = nhdsWithin x s

theorem OpenPartialHomeomorph.nhdsWithin_target_inter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) (s : Set Y) : nhdsWithin x (e.target ∩ s) = nhdsWithin x s

theorem OpenPartialHomeomorph.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (h : x ∈ e.source) : ContinuousAt (↑e) x

An open partial homeomorphism is continuous at any point of its source

theorem OpenPartialHomeomorph.continuousAt_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ContinuousAt (↑e.symm) x

An open partial homeomorphism inverse is continuous at any point of its target

theorem OpenPartialHomeomorph.tendsto_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.Tendsto (↑e.symm) (nhds (↑e x)) (nhds x)

theorem OpenPartialHomeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.map (↑e) (nhds x) = nhds (↑e x)

theorem OpenPartialHomeomorph.symm_map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.map (↑e.symm) (nhds (↑e x)) = nhds x

theorem OpenPartialHomeomorph.image_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) {s : Set X} (hs : s ∈ nhds x) : ↑e '' s ∈ nhds (↑e x)

theorem OpenPartialHomeomorph.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set X) : Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) (↑e '' (e.source ∩ s))

theorem OpenPartialHomeomorph.map_nhdsWithin_preimage_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set Y) : Filter.map (↑e) (nhdsWithin x (↑e ⁻¹' s)) = nhdsWithin (↑e x) s

theorem OpenPartialHomeomorph.eventually_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p y) ↔ ∀ᶠ (x : X) in nhds x, p (↑e x)

theorem OpenPartialHomeomorph.eventually_nhds' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x

theorem OpenPartialHomeomorph.eventually_nhdsWithin {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p y) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p (↑e x)

theorem OpenPartialHomeomorph.eventually_nhdsWithin' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p x

theorem OpenPartialHomeomorph.preimage_eventuallyEqSet_target_inter_preimage_inter {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

This lemma is useful in the manifold library in the case that e is a chart. It states that locally around e x the set e.symm ⁻¹' s is the same as the set intersected with the target of e and some other neighborhood of f x (which will be the source of a chart on Z).

@[deprecated OpenPartialHomeomorph.preimage_eventuallyEqSet_target_inter_preimage_inter (since := "2026-08-14")]

theorem OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Alias of OpenPartialHomeomorph.preimage_eventuallyEqSet_target_inter_preimage_inter.

---

This lemma is useful in the manifold library in the case that e is a chart. It states that locally around e x the set e.symm ⁻¹' s is the same as the set intersected with the target of e and some other neighborhood of f x (which will be the source of a chart on Z).

theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} {x : Y} (h : x ∈ e.target) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)

Continuity within a set at a point can be read under right composition with a local homeomorphism, if the point is in its target

theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {x : Y} (h : x ∈ e.target) : ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Continuity at a point can be read under right composition with an open partial homeomorphism, if the point is in its target

theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} (h : s ⊆ e.target) : ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)

A function is continuous on a set if and only if its composition with an open partial homeomorphism on the right is continuous on the corresponding set.

theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z} {x : Z} (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ nhdsWithin x s) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x

Continuity within a set at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism

theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {x : Z} (h : f ⁻¹' e.source ∈ nhds x) : ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Continuity at a point can be read under left composition with an open partial homeomorphism if a neighborhood of the initial point is sent to the source of the partial homeomorphism

theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z} (h : s ⊆ f ⁻¹' e.source) : ContinuousOn f s ↔ ContinuousOn (↑e ∘ f) s

A function is continuous on a set if and only if its composition with an open partial homeomorphism on the left is continuous on the corresponding set.

theorem OpenPartialHomeomorph.continuous_iff_continuous_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} (h : f ⁻¹' e.source = Set.univ) : Continuous f ↔ Continuous (↑e ∘ f)

A function is continuous if and only if its composition with an open partial homeomorphism on the left is continuous and its image is contained in the source.