ContinuousOn Compacts implies Continuous

Stream: Is there code for X?

[David Ledvinka]

I would like something like

import Mathlib.Topology.Defs.Filter

example {X Y : Type*} [TopologicalSpace X] [LocallyCompactSpace X] [TopologicalSpace Y]
  {f : X → Y} (h : ∀ K : Set X, IsCompact K → ContinuousOn f K) : Continuous f := by sorry

More generally I see that there is some glueing lemmas in mathlib but as far as I could tell none are statement in a form where the hypothesis is ContinuousOn (for example it suffices to check continuity on a basis of the topology).

[Aaron Liu]

import Mathlib.Topology.ContinuousOn

example {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y]
    {f : X → Y} (h : ∀ K : Set X, IsCompact K → ContinuousOn f K) : Continuous f := by
  rw [continuous_iff_continuousAt]
  intro x
  obtain ⟨K, hK, hx⟩ := exists_compact_mem_nhds x
  exact (h K hK).continuousAt hx

[David Ledvinka]

Do you think this should go in mathlib or just be inlined?

[Aaron Liu]

I have no idea

[Kevin Buzzard]

If you have a use for it and it's not already there, I think that's an argument for adding it.

[Anatole Dedecker]

This "exists" as a combination of docs#Topology.IsCoherentWith.continuous_iff and docs#Topology.IsCoherentWith.isCompact_of_weaklyLocallyCompact. But the true lemma will come out of #21237 (which I'm having a look at right now).