instTopologicalSpaceStoneCech — Mathlib

English

The topology on StoneCech α is the quotient topology induced by the quotient map T2Quotient.mk : PreStoneCech α → StoneCech α.

Русский

Топология на StoneCech α есть тождественная квотиентная топология, индуцированная отображением T2Quotient.mk : PreStoneCech α → StoneCech α.

LaTeX

$$$ \text{TopologicalSpace}(StoneCech \alpha) \text{ is induced by } T2Quotient.mk : PreStoneCech \alpha \to StoneCech \alpha $$$

Lean4

instance : TopologicalSpace (StoneCech α) :=
  inferInstanceAs <| TopologicalSpace <| T2Quotient _

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