English
Every sequential space is compactly generated.
Русский
Каждое последовательное пространство является компактно-генерированным.
LaTeX
$$$\\text{SequentialSpace}(X) \\Rightarrow \\text{CompactlyGeneratedSpace}(X)$$$
Lean4
/-- A sequential space is compactly generated.
The proof is taken from <https://ncatlab.org/nlab/files/StricklandCGHWSpaces.pdf>,
Proposition 1.6. -/
instance (priority := 100) [SequentialSpace X] : UCompactlyGeneratedSpace.{u} X :=
by
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ SequentialSpace.isClosed_of_seq _ fun u p hu hup ↦ ?_
let g : ULift.{u} (OnePoint ℕ) → X := (continuousMapMkNat u p hup) ∘ ULift.down
change ULift.up ∞ ∈ g ⁻¹' s
have : Filter.Tendsto (@OnePoint.some ℕ) Filter.atTop (𝓝 ∞) :=
by
rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]
exact tendsto_coe_infty
apply IsClosed.mem_of_tendsto _ ((continuous_uliftUp.tendsto ∞).comp this)
· simp only [Function.comp_apply, mem_preimage, eventually_atTop, ge_iff_le]
exact ⟨0, fun b _ ↦ hu b⟩
·
exact
h (CompHaus.of (ULift.{u} (OnePoint ℕ))) ⟨g, (continuousMapMkNat u p hup).continuous.comp continuous_uliftDown⟩
