secondCountableTopology — Mathlib

English

Let X be a second countable space and q: X → Quotient S be an open quotient map. Then the quotient space Quotient S is second countable.

Русский

Пусть X — пространство с второй счётностью, и q: X → Quotient S — открытое отображение на фактор-пространство Quotient S. Тогда Quotient S является вторократно счётным топологическим пространством.

LaTeX

$$$SecondCountableTopology X \rightarrow IsOpenMap(Quotient.mk' : X \to Quotient S) \rightarrow SecondCountableTopology (Quotient S).$$$

Lean4

/-- An open quotient of a second countable space is second countable. -/
theorem secondCountableTopology [SecondCountableTopology X] (h : IsOpenMap (Quotient.mk' : X → Quotient S)) :
    SecondCountableTopology (Quotient S) :=
  isQuotientMap_quotient_mk'.secondCountableTopology h

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