Continuity of inverses of maps out of compact sets

A continuous injection from a compact space to a Hausdorff space is a closed embedding. This file records the version of that fact needed for the characteristic maps of cells: let f be continuous on a compact set K, with values in a Hausdorff space, injective on a subset U ⊆ K, and assume no point of K \ U has the same image as a point of U. Then the inverse Function.invFunOn f U is continuous on f '' U (ContinuousOn.continuousOn_invFunOn_image_of_isCompact). For a cell, K is the closed unit ball, U the open unit ball, and the boundary sphere is mapped outside the open cell.

The proof is the closed map argument: the preimage under the inverse of a closed set C is the trace on f '' U of the compact, hence closed, set f '' (C ∩ K).

theorem ContinuousOn.continuousOn_invFunOn_image_of_isCompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Nonempty α] [T2Space β] {f : α → β} {K U : Set α} (hf : ContinuousOn f K) (hK : IsCompact K) (hUK : U ⊆ K) (hinj : Set.InjOn f U) (hdisj : Disjoint (f '' (K \ U)) (f '' U)) : ContinuousOn (Function.invFunOn f U) (f '' U)

Inverses of maps out of compact sets are continuous. If f is continuous on a compact set K with values in a Hausdorff space, injective on U ⊆ K, and no point of K \ U has the same image as a point of U, then the inverse invFunOn f U of f on U is continuous on f '' U.