continuous_from_compactlyGenerated

English

If X is compactly generated, then a map f: X → Y is continuous provided that f ∘ g is continuous for every continuous g from any compact Hausdorff S.

Русский

Если X компактно-генерируемое, то отображение f: X → Y непрерывно, если для каждого компактного хаусдорфовского пространства S и каждого непрерывного g: S → X композиция f ∘ g непрерывна.

LaTeX

$$$ \forall f:\, X \to Y,\ (\forall (S : CompHaus) (g : C(S, X)),\, Continuous (f \circ g)) \Rightarrow \operatorname{Continuous}(f) $$$

Lean4

theorem continuous_from_compactlyGenerated [TopologicalSpace X] [t : TopologicalSpace Y] (f : X → Y)
    (h : ∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) : Continuous[compactlyGenerated.{u} X, t] f :=
  by
  rw [continuous_coinduced_dom]
  continuity

Похожие утверждения