eq_generateFrom_countableBasis — Mathlib

English

In a second-countable space α, the topology t on α is generated by the countable basis countableBasis α.

Русский

В пространстве с второй счётностью α топология t порождается базисом countableBasis α.

LaTeX

$$$\text{topology } t = \text{generateFrom}(\text{countableBasis}(\alpha))$$$

Lean4

theorem eq_generateFrom_countableBasis [SecondCountableTopology α] :
    ‹TopologicalSpace α› = generateFrom (countableBasis α) :=
  (isBasis_countableBasis α).eq_generateFrom

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