English
A Hausdorff space is compactly generated if to prove that s is open it suffices to show that for every compact K ⊆ X, s ∩ K is open in K.
Русский
Пусть пространство хаусдорфово. Чтобы доказать, что s открыто, достаточно показать, что для каждого компактного K ⊆ X множество s ∩ K открыто в K.
LaTeX
$$$\\text{CompactlyGeneratedSpace}(X) \\Rightarrow \\left( \\forall s, \\forall K [\\\\text{IsCompact}(K)], IsOpen (s \\cap K) \\Rightarrow IsOpen(s)\\right)$$$
Lean4
/-- Let `s ⊆ X`. Suppose that `X` is Hausdorff, and that to prove that `s` is open,
it suffices to show that for every compact set `K ⊆ X`, `s ∩ K` is open in `K`.
Then `X` is compactly generated. -/
theorem compactlyGeneratedSpace_of_isOpen_of_t2 (h : ∀ s, (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s) :
CompactlyGeneratedSpace X :=
by
refine compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
exact hs _ Subtype.val continuous_subtype_val
