English
Let X be Hausdorff. If the closedness of s can be checked on all compact subsets K by verifying that s ∩ K is closed, then X is compactly generated.
Русский
Пусть X — хаусдорфово. Если замкнутость множества s можно проверить на каждом компактномK путём проверки, что s ∩ K замкнуто, тогда X компактно-генерировано.
LaTeX
$$$h: \\forall s, (\\forall K, IsCompact(K) \\to IsClosed(s \\cap K)) \\to IsClosed(s) \\Rightarrow \\operatorname{CompactlyGeneratedSpace}(X)$$$
Lean4
/-- Let `s ⊆ X`. Suppose that `X` is Hausdorff, and that to prove that `s` is closed,
it suffices to show that for every compact set `K ⊆ X`, `s ∩ K` is closed.
Then `X` is compactly generated. -/
theorem compactlyGeneratedSpace_of_isClosed_of_t2
(h : ∀ s, (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s) : CompactlyGeneratedSpace X :=
by
refine compactlyGeneratedSpace_of_isClosed fun s hs ↦ h s fun K hK ↦ ?_
rw [Set.inter_comm, ← Subtype.image_preimage_coe]
apply hK.isClosed.isClosedMap_subtype_val
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
exact hs _ Subtype.val continuous_subtype_val
