English
If a space X satisfies the property that every A is open whenever for all compact K the preimage of A under the inclusion map is open, then X is compactly coherent.
Русский
Если пространство X обладает свойством, что для любого множества A выполняется: если для всех компактных K прообраз A по включению открыт, то A открыто, тогда X компактно-согласовано.
LaTeX
$$$ \forall A \subseteq X,\ (\forall K,\operatorname{IsCompact}(K) \Rightarrow \operatorname{IsOpen}(K \downarrow \cap A)) \Rightarrow \operatorname{IsOpen}(A) $$$
Lean4
/-- If every set `A` is open if for every compact `K` the intersection `K ∩ A` is open in `K`,
then the space is a compactly coherent space. -/
theorem of_isOpen (h : ∀ (A : Set X), (∀ K, IsCompact K → IsOpen (K ↓∩ A)) → IsOpen A) : CompactlyCoherentSpace X where
isCoherentWith := { isOpen_of_forall_induced := h }
