instTopologicalSpaceSigma — Mathlib

English

The quotient space (Quotient s) carries the quotient topology induced by the canonical quotient map Quotient.mk'.

Русский

Фактор-пространство (Quotient s) имеет факторную топологию, индуцированную канонической картой-квотированием Quotient.mk'.

LaTeX

$$$\\text{TopologicalSpace}(\\mathrm{Quotient}(s)) = \\mathrm{coinduced}(\\mathrm{Quotient.mk'}, \\text{TopologicalSpace}(X))$$$

Lean4

instance instTopologicalSpaceSigma {ι : Type*} {X : ι → Type v} [t₂ : ∀ i, TopologicalSpace (X i)] :
    TopologicalSpace (Sigma X) :=
  ⨆ i, coinduced (Sigma.mk i) (t₂ i)

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