instSequentialSpace — Mathlib

English

The quotient of a sequential space is sequential (Quotient.space).

Русский

Квотиент последовательного пространства остаётся последовательным.

LaTeX

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

Lean4

/-- The quotient of a sequential space is a sequential space. -/
instance instSequentialSpace [SequentialSpace X] {s : Setoid X} : SequentialSpace (Quotient s) :=
  isQuotientMap_quot_mk.sequentialSpace

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