isClosed_iff_of_t2 — Mathlib

English

Let X be a Hausdorff compactly generated space. A subset s is closed iff s ∩ K is closed for every compact K ⊆ X.

Русский

Пусть X — хаусдорфово компактно-генерируемое пространство. Подмножество s замкнуто тогда и только тогда, когда s ∩ K замкнуто для каждого компактного K ⊆ X.

LaTeX

$$$[\\text{CompactlyGeneratedSpace } X] \\;\\&\\; [\\text{T2Space } X] \\;\\Rightarrow \\text{IsClosed}(s) \\iff \\forall \\{K: Set X\\}, IsCompact(K) \\to IsClosed(s \\cap K)$$$

Lean4

theorem isClosed_iff_of_t2 [CompactlyGeneratedSpace X] (s : Set X) : IsClosed s ↔ ∀ ⦃K⦄, IsCompact K → IsClosed (s ∩ K)
    where
  mp hs _ hK := hs.inter hK.isClosed
  mpr := CompactlyGeneratedSpace.isClosed

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