to_firstCountableTopology — Mathlib

English

If β is second-countable, then for any map f: α → β, the topology on α induced by f is first-countable.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) to_firstCountableTopology [SecondCountableTopology α] : FirstCountableTopology α :=
  ⟨fun _ =>
    HasCountableBasis.isCountablyGenerated <|
      ⟨(isBasis_countableBasis α).nhds_hasBasis, (countable_countableBasis α).mono inter_subset_left⟩⟩
    -- see Note [lower instance priority]

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