English
If t1 and t2 are sequential topologies on X, then their supremum t1 ⊔ t2 is sequential.
Русский
Если на X заданы две последовательные топологии t1 и t2, то их наибольшая сумма t1 ⊔ t2 также последовательна.
LaTeX
$$$\text{SequentialSpace}(X) \Rightarrow \text{SequentialSpace}(X, t_1) \land \text{SequentialSpace}(X, t_2) \Rightarrow \text{SequentialSpace}(X, t_1 \sqcup t_2)$$$
Lean4
protected theorem iSup {X} {ι : Sort*} {t : ι → TopologicalSpace X} (h : ∀ i, @SequentialSpace X (t i)) :
@SequentialSpace X (⨆ i, t i) := by
letI : TopologicalSpace X := ⨆ i, t i
refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩
letI := t i
exact IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _
