instUCompactlyGeneratedSpaceQuotient

English

The quotient of a compactly generated space by a Setoid is compactly generated.

Русский

Факторпространство компактно-генерируемого пространства по отношению эквивалентности является компактно-генерируемым.

LaTeX

$$$ \forall {S : \text{Setoid } X},\ [\operatorname{UCompactlyGeneratedSpace}(X)] \Rightarrow \operatorname{UCompactlyGeneratedSpace}(\operatorname{Quotient}(S)) $$$

Lean4

/-- The quotient of a compactly generated space is compactly generated. -/
instance {S : Setoid X} [UCompactlyGeneratedSpace.{u} X] : UCompactlyGeneratedSpace.{u} (Quotient S) :=
  uCompactlyGeneratedSpace_of_coinduced continuous_quotient_mk' rfl

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