secondCountableTopology — Mathlib

English

If f: α → β is an inducing map and β is second countable, then α is second countable.

Русский

Если отображение f: α → β индуцирует топологию на α и β имеет вторую счётность, то α имеет вторую счётность.

LaTeX

$$$IsInducing f \rightarrow SecondCountableTopology \beta \rightarrow SecondCountableTopology \alpha$$$

Lean4

protected theorem secondCountableTopology [TopologicalSpace β] [SecondCountableTopology β] (hf : IsInducing f) :
    SecondCountableTopology α := by
  rw [hf.1]
  exact secondCountableTopology_induced α β f

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