English
If a space X satisfies that a set s is open whenever for all compact spaces K the preimage of s under the natural map is open, then X is compactly coherent.
Русский
Если пространство X удовлетворяет условию, что множество s открыто тогда и только тогда, когда для всех компактных пространств K их естественные отображения дают открытое прообраз, то X компактно-согласовано.
LaTeX
$$$ \forall s,\ (\forall K,\operatorname{IsCompact}(K) \rightarrow \operatorname{IsOpen}(\operatorname{preimage}(\text{incl}, s))) \Rightarrow \operatorname{IsOpen}(s) $$$
Lean4
/-- A topological space `X` is compactly coherent if a set `s` is open when `f ⁻¹' s?` is open for
every continuous map `f : K → X`, where `K` is compact. -/
theorem of_isOpen_forall_compactSpace
(h :
∀ (s : Set X),
(∀ (K : Type u) [TopologicalSpace K], [CompactSpace K] → ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) →
IsOpen s) :
CompactlyCoherentSpace X := by
refine of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_
specialize hA (range f) (isCompact_range hf)
have := hA.preimage (hf.codRestrict mem_range_self)
rwa [← preimage_comp] at this
