compactlyGeneratedSpace_of_isOpen

English

In a compactly generated space, a set s is open if s ∩ K is open for every compact K.

Русский

В компактно-генерируемом пространстве множество s открыто тогда и только тогда, когда s ∩ K открыто для каждого компактного K.

LaTeX

$$[CompactlyGeneratedSpace X] → ∀ {s}, (∀ ⦃K⦄, IsCompact K → IsOpen (s ∩ K)) → IsOpen s$$

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 compactlyGeneratedSpace_of_isOpen
    (h :
      ∀ (s : Set X),
        (∀ (K : Type u) [TopologicalSpace K],
            [CompactSpace K] → [T2Space K] → ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) →
          IsOpen s) :
    CompactlyGeneratedSpace X :=
  uCompactlyGeneratedSpace_of_isOpen fun s h' ↦ h s fun K _ _ _ f hf ↦ h' (CompHaus.of K) ⟨f, hf⟩

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