map_nhds_induced_eq — Mathlib

English

For a ∈ α, map f (nhds a) equals nhdsWithin (range f) (f a) when using induced topology by f.

Русский

Для фиксированного a: α отображение map f от nhds a равно nhdsWithin (range f) (f a) в индуцированной топологии через f.

LaTeX

$$$\\text{map } f (\\mathcal{N}_{\\mathrm{induced}\\ f\\ t}(a)) = \\mathcal{N}_{\\mathrm{within}} (\\mathrm{range}(f)) (f(a)).$$$

Lean4

theorem map_nhds_induced_eq (a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a := by
  rw [nhds_induced, Filter.map_comap, nhdsWithin]

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