secondCountableTopology_induced — Mathlib

English

The induced topology on α by any map f: α → β is second-countable when β is.

Русский

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

LaTeX

$$$\forall f:\alpha \to \beta,\; @SecondCountableTopology\alpha(t.induced f)$$$

Lean4

/-- If `β` is a second-countable space, then its induced topology via
`f` on `α` is also second-countable. -/
theorem secondCountableTopology_induced (α β) [t : TopologicalSpace β] [SecondCountableTopology β] (f : α → β) :
    @SecondCountableTopology α (t.induced f) :=
  by
  rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
  letI := t.induced f
  refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
  rw [eq, induced_generateFrom_eq]

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