induced_iff_nhds_eq — Mathlib

English

Two topologies tα on α and tβ on β satisfy tβ = tα.induced f if and only if for every b ∈ β, nhds b equals comap f (nhds(f(b))).

Русский

Две топологии tα на α и tβ на β удовлетворяют tβ = tα.induced f тогда и только тогда, когда для каждого b ∈ β окрестности b равны comap f (окрестности f(b)).

LaTeX

$$$t_\\beta = t_\\alpha^{\\text{induced } f} \\iff \\forall b,\\; 𝓝 b = \\operatorname{comap} f (𝓝 (f b)).$$$

Lean4

theorem induced_iff_nhds_eq [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
    tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b) := by simp only [ext_iff_nhds, nhds_induced]

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