of_isClosed — Mathlib

English

If a space X has the property that for every A, whenever for all compact K the preimage of A is closed, then A is closed, then X is compactly coherent.

Русский

Если пространство X удовлетворяет свойству: для любого A, если для всех компактных K прообраз A замкнут, то A замкнуто, тогда X компактно-согласовано.

LaTeX

$$$ \forall A,\ (\forall K,\operatorname{IsCompact}(K) \Rightarrow \operatorname{IsClosed}(K \downarrow \cap A)) \Rightarrow \operatorname{IsClosed}(A) $$$

Lean4

/-- If every set `A` is closed if for every compact `K` the intersection `K ∩ A` is closed in `K`,
then the space is a compactly coherent space. -/
theorem of_isClosed (h : ∀ (A : Set X), (∀ K, IsCompact K → IsClosed (K ↓∩ A)) → IsClosed A) : CompactlyCoherentSpace X
    where isCoherentWith := IsCoherentWith.of_isClosed h

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