Images of closed sets under maps tending to infinity

Let f be continuous on a closed subset A of a proper metric space. The image of each bounded part of A is then bounded, since its closure in A is compact, so any choice of preimages of points escaping to infinity escapes to infinity as well. If moreover f tends to infinity at infinity along A, then f '' A is closed, and when f is injective on A its inverse on f '' A is continuous: f restricted to A is a closed embedding.

These facts let a map defined on a closed region, such as the closed upper half-plane, be inverted continuously up to the boundary of its image.

Main results

• TauCeti.tendsto_invFunOn_cobounded: chosen preimages of points escaping to infinity escape to infinity.
• TauCeti.isClosed_image_of_tendsto_cobounded: f '' A is closed when f tends to infinity at infinity along A.
• TauCeti.continuousOn_of_leftInvOn_of_tendsto_cobounded: any left inverse on A of such an f, for instance invFunOn f A when f is injective on A, is continuous on f '' A.

theorem TauCeti.tendsto_invFunOn_cobounded {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {f : α → β} {A : Set α} [Nonempty α] [PseudoMetricSpace β] (hA : IsClosed A) (hf : ContinuousOn f A) : Filter.Tendsto (Function.invFunOn f A) (Bornology.cobounded β ⊓ Filter.principal (f '' A)) (Bornology.cobounded α)

If f is continuous on a closed subset A of a proper space, then any choice of preimages in A of points of f '' A escaping to infinity escapes to infinity.

theorem TauCeti.isClosed_image_of_tendsto_cobounded {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {f : α → β} {A : Set α} [MetricSpace β] (hA : IsClosed A) (hf : ContinuousOn f A) (hp : Filter.Tendsto f (Bornology.cobounded α ⊓ Filter.principal A) (Bornology.cobounded β)) : IsClosed (f '' A)

Images of closed sets under maps tending to infinity are closed. If f is continuous on a closed subset A of a proper space and tends to infinity at infinity along A, then f '' A is closed.

theorem TauCeti.continuousOn_of_leftInvOn_of_tendsto_cobounded {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {f : α → β} {A : Set α} [MetricSpace β] {g : β → α} (hA : IsClosed A) (hf : ContinuousOn f A) (hg : Set.LeftInvOn g f A) (hp : Filter.Tendsto f (Bornology.cobounded α ⊓ Filter.principal A) (Bornology.cobounded β)) : ContinuousOn g (f '' A)

Continuity of the inverse of a map tending to infinity. If f is continuous on a closed subset A of a proper space and tends to infinity at infinity along A, then any left inverse g of f on A is continuous on f '' A. For f injective on A, this applies to invFunOn f A via Set.InjOn.leftInvOn_invFunOn.