sequentialSpace

Mathlib.Topology.Sequences

URI: https://scilib.ai/kg/mathlib#Topology.IsQuotientMap.sequentialSpace

English

The quotient of a sequential space is sequential.

Русский

Квотие пространства, являющегося последовательным, тоже последовательно.

LaTeX

$$$\text{SequentialSpace}(X) \Rightarrow \text{SequentialSpace}(\mathrm{Quotient}\; s)$$$

Lean4

theorem sequentialSpace [SequentialSpace X] {f : X → Y} (hf : IsQuotientMap f) : SequentialSpace Y :=
  hf.2.symm ▸ .coinduced f

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru