Inverses of continuous families of equivalences

For a family of equivalences from a compact space to a Hausdorff space, joint continuity of forward evaluation implies joint continuity of inverse evaluation. This is the parametric form of Mathlib's Continuous.continuous_symm_of_equiv_compact_to_t2; in particular it applies to families of homeomorphisms. It allows inverse points to vary continuously without imposing a topology on the type of equivalences itself. The proof uses Mathlib's compact-codomain closed-graph criterion continuous_of_isClosed_graph.

theorem TauCeti.continuous_equiv_symm_eval {P : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace P] [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] (e : P → X ≃ Y) (he : Continuous fun (p : P × X) => (e p.1) p.2) : Continuous fun (p : P × Y) => (e p.1).symm p.2

Inverse evaluation is jointly continuous for a family of equivalences from a compact space to a Hausdorff space whose forward evaluation is jointly continuous. The parameter space is arbitrary.