map_nhds — Mathlib

English

The image filter of a neighborhood under a function is the infimum over images of open neighborhoods.

Русский

Образ фильтра окрестностей под функцией равен инфимууму образов открытых окрестностей.

LaTeX

$$$\\text{map}_f(\\mathcal N(x)) = \\bigwedge_{s\\ni x,\\ IsOpen(s)} \\mathcal P(f''s)$$$

Lean4

theorem map_nhds {f : X → α} : map f (𝓝 x) = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, 𝓟 (f '' s) :=
  ((nhds_basis_opens x).map f).eq_biInf

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