nhds_induced — Mathlib

English

For any f: β → α, a ∈ β, the neighborhood filter on β in the induced topology is the comap of f of the neighborhood filter at f(a): nhds β (induced f T) a = comap f (nhds (f a)).

Русский

Для отображения f: β → α и элемента a ∈ β фильтр окрестностей в индуцированной топологии равен префильтру: nhds β (induced f T) a = comap f (nhds (f a)).

LaTeX

$$$\\text{nhds } a = \\operatorname{comap} f (\\mathcal{N}(f a)).$$$

Lean4

theorem nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) :
    @nhds β (TopologicalSpace.induced f T) a = comap f (𝓝 (f a)) :=
  by
  ext s
  rw [mem_nhds_induced, mem_comap]

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