English
In a compactly coherent space, a set s is open iff for every compact K, the preimage of s under any continuous map from K is open in K.
Русский
В компактно-согласованном пространстве множество s открыто тогда и только тогда, когда прообраз s под любым непрерывным отображением из любого компактного K открыто в K.
LaTeX
$$$ \forall s, \operatorname{IsOpen}(s) \iff \forall K [\operatorname{IsCompact}(K)],\ IsOpen(f^{-1}(s)) $$$
Lean4
/-- In a compactly coherent space `X`, a set `s` is open iff `f ⁻¹' s` is open for every continuous
map from a compact space. -/
theorem isOpen_iff_forall_compactSpace [CompactlyCoherentSpace X] (s : Set X) :
IsOpen s ↔ ∀ (K : Type u) [TopologicalSpace K] [CompactSpace K], ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s) :=
by
refine ⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩
intro K hK
have : CompactSpace K := isCompact_iff_compactSpace.mp hK
exact hs K Subtype.val continuous_subtype_val
