isClosed_iff — Mathlib

English

In a compactly coherent space, A is closed iff for every compact K, the intersection K ∩ A is closed in K.

Русский

В компактно-согласованном пространстве множество A замкнуто тогда и только тогда, когда для каждого компактного K пересечение K ∩ A замкнуто в K.

LaTeX

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

Lean4

/-- A set `A` in a compactly coherent space is closed iff for every compact set `K`, the
intersection `K ∩ A` is closed in `K`. -/
theorem isClosed_iff [CompactlyCoherentSpace X] (A : Set X) : IsClosed A ↔ ∀ K, IsCompact K → IsClosed (K ↓∩ A) :=
  IsCoherentWith.isClosed_iff isCoherentWith

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