English
Let f: X → Y. If for every compact Hausdorff space S and every continuous g: S → X, f ∘ g is continuous, then f is continuous from the compactly generated structure of X.
Русский
Пусть f: X → Y. Если для каждого компактного хаусдорфова пространства S и каждого непрерывного g: S → X композиция f ∘ g непрерывна, то f непрерывно по компактно-генерируемой структуре X.
LaTeX
$$$ \forall f:X \to Y,\ (\forall (S:CompHaus) (g:C(S,X)), Continuous (f \circ g)) \Rightarrow \operatorname{Continuous}(f) $$$
Lean4
/-- Let `f : X → Y`. Suppose that to prove that `f` is continuous, it suffices to show that
for every compact Hausdorff space `K` and every continuous map `g : K → X`, `f ∘ g` is continuous.
Then `X` is compactly generated. -/
theorem uCompactlyGeneratedSpace_of_continuous_maps [t : TopologicalSpace X]
(h :
∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
(∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) → Continuous f) :
UCompactlyGeneratedSpace.{u} X where
le_compactlyGenerated :=
by
suffices Continuous[t, compactlyGenerated.{u} X] (id : X → X) by rwa [← continuous_id_iff_le]
apply h (tY := compactlyGenerated.{u} X)
intro S g
let f : (Σ (i : (T : CompHaus.{u}) × C(T, X)), i.fst) → X := fun ⟨⟨_, i⟩, s⟩ ↦ i s
suffices
∀ (i : (T : CompHaus.{u}) × C(T, X)), Continuous[inferInstance, compactlyGenerated X] (fun (a : i.fst) ↦ f ⟨i, a⟩)
from this ⟨S, g⟩
rw [← @continuous_sigma_iff]
apply continuous_coinduced_rng
