English
If X is sequential and S contains every set of the form insert x (range u) where u is a sequence converging to x, then the topology is generated by the restrictions to the sets in S.
Русский
Если X — последовательностное пространство и S содержит каждое множество вида insert x (range u), где u — последовательность, сходящаяся к x, тогда топология задается ограничениями на множества из S.
LaTeX
$$$ [SequentialSpace X] \\to (\\forall u : \\mathbb{N} \\to X, {\\rm Tendsto}\\ u \\mathrm{atTop} \\mathcal{N}(x) \\to \\mathrm{insert}\, x\, (\\mathrm{range}\, u) \\in S) \\to \\text{IsCoherentWith } S $$$
Lean4
/-- If `X` is a sequential space
and `S` contains each set of the form `insert x (Set.range u)`
where `u : ℕ → X` is a sequence and `x` is its limit,
then topology on `X` is generated by its restrictions to the sets of `S`. -/
theorem of_seq [SequentialSpace X] (h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S) :
IsCoherentWith S := by
refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_
rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩
rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst
suffices x ∈ s by specialize hst x; simp_all
refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_
specialize hst (u k)
simp_all
