firstCountableTopology_induced — Mathlib

English

If β is a first-countable space and f: α → β is any map, then the induced topology on α via f is also first-countable.

Русский

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

LaTeX

$$$\text{FirstCountableTopology} \bigl(\text{t.induced}(f)\bigr)$$$

Lean4

/-- If `β` is a first-countable space, then its induced topology via `f` on `α` is also
first-countable. -/
theorem firstCountableTopology_induced (α β : Type*) [t : TopologicalSpace β] [FirstCountableTopology β] (f : α → β) :
    @FirstCountableTopology α (t.induced f) :=
  let _ := t.induced f
  ⟨fun x ↦ nhds_induced f x ▸ inferInstance⟩

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