tendsto_lift'_closure_nhds — Mathlib

English

For a continuous map f, and any x, Tendsto f from the nhds x lifted with closure to nhds(fx) lifted with closure.

Русский

Для непрерывного отображения f и любого x предел существует между nhds x и nhds(f(x)) с замыканием.

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow \\forall x,\\ Tendsto\\ f\\ ((\\mathcal{N}x)^{\\uparrow}\\mathrm{closure})\\ ((\\mathcal{N}(f x))^{\\uparrow}\\mathrm{closure})$$$

Lean4

theorem tendsto_lift'_closure_nhds (hf : Continuous f) (x : X) :
    Tendsto f ((𝓝 x).lift' closure) ((𝓝 (f x)).lift' closure) :=
  (hf.tendsto x).lift'_closure hf

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