English
In a compactly generated space, a set s is open if for every compact K and every continuous f: K → X, the preimage f^{-1}(s) is open.
Русский
В компактно-генерируемом пространстве множество s открыто тогда, когда для каждого компактного K и каждого непрерывного отображения f: K → X множество f^{-1}(s) открыто.
LaTeX
$$[CompactlyGeneratedSpace X] ⟹ (∶ ∀ (K : Type u) [TopologicalSpace K], [CompactSpace K] → [T2Space K] → ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s$$
Lean4
/-- In a compactly generated space `X`, a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem isOpen' [CompactlyGeneratedSpace X] {s : Set X}
(hs :
∀ (K : Type u) [TopologicalSpace K],
[CompactSpace K] → [T2Space K] → ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) :
IsOpen s :=
UCompactlyGeneratedSpace.isOpen fun S ⟨f, hf⟩ ↦ hs S f hf
