Continuity and punctured neighbourhoods under open partial homeomorphisms

An open partial homeomorphism identifies a neighbourhood of a point of its source with a neighbourhood of its image, so a point of the source is not isolated as soon as its image is not (OpenPartialHomeomorph.nhdsNE_neBot). For instance, no point in the source of a chart into a nontrivially normed field is isolated. Being injective and continuous on its source, it sends the punctured neighbourhoods of a point of its source to those of the image (OpenPartialHomeomorph.tendsto_nhdsNE). Eventual constancy of a map f near x is likewise detected by its chart representative e' ∘ f ∘ e.symm near e x (OpenPartialHomeomorph.not_eventuallyConst_comp_symm).

A continuous function on the target that is constant off a compact subset of the target, read through the open partial homeomorphism on its source and extended by that constant, is continuous on a Hausdorff domain (OpenPartialHomeomorph.continuous_ite_source_of_eq_off_compact). This transplants a compactly supported function on a chart to the whole space.

theorem OpenPartialHomeomorph.nhdsNE_neBot {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) [(nhdsWithin (↑e x) {↑e x}ᶜ).NeBot] : (nhdsWithin x {x}ᶜ).NeBot

A point of the source of an open partial homeomorphism is not isolated if its image is not.

theorem OpenPartialHomeomorph.tendsto_nhdsNE {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) (nhdsWithin x {x}ᶜ) (nhdsWithin (↑e x) {↑e x}ᶜ)

An open partial homeomorphism sends the punctured neighbourhoods of a point of its source to the punctured neighbourhoods of its image.

theorem OpenPartialHomeomorph.continuous_ite_source_of_eq_off_compact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (e : OpenPartialHomeomorph X Y) [(z : X) → Decidable (z ∈ e.source)] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hg : Continuous g) {K : Set Y} (hK : IsCompact K) (hKt : K ⊆ e.target) {c : Z} (hgK : ∀ z ∉ K, g z = c) : Continuous fun (z : X) => if z ∈ e.source then g (↑e z) else c

A continuous function g equal to c off a compact subset K of the target of e, read through e on its source and extended by c, is continuous when the domain is Hausdorff.

theorem OpenPartialHomeomorph.not_eventuallyConst_comp_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} {W : Type u_4} [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {x : X} (e : OpenPartialHomeomorph X Z) {e' : OpenPartialHomeomorph Y W} (hx : x ∈ e.source) (hZ2 : ∀ᶠ (z : Z) in nhds (↑e x), f (↑e.symm z) ∈ e'.source) (hne : ¬Filter.EventuallyConst f (nhds x)) : ¬Filter.EventuallyConst (fun (z : Z) => ↑e' (f (↑e.symm z))) (nhds (↑e x))

If f is not eventually constant near x, then its chart representative e' ∘ f ∘ e.symm is not eventually constant near e x, provided f ∘ e.symm maps a neighbourhood of e x into the source of e'.