uCompactlyGeneratedSpace_of_isOpen

English

Alternative formulation: the sigma-type CG property holds for the sum type as well as for the sigma construction itself.

Русский

Альтернативная формулировка: свойство компактно-генерируемого пространства справедливо и для суммы, и для сигма-конструкции.

LaTeX

$$$ \text{(same CG sigma statement in alternative form)} $$$

Lean4

/-- A topological space `X` is compactly generated if a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem uCompactlyGeneratedSpace_of_isOpen
    (h : ∀ (s : Set X), (∀ (S : CompHaus.{u}) (f : C(S, X)), IsOpen (f ⁻¹' s)) → IsOpen s) :
    UCompactlyGeneratedSpace.{u} X :=
  uCompactlyGeneratedSpace_of_continuous_maps fun _ h' ↦ continuous_def.2 fun _ hs ↦ h _ fun S g ↦ hs.preimage (h' S g)

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