extend_eq_of_tendsto — Mathlib

English

If Tendsto f (comap i (nhds b)) (nhds c), then di.extend f b = c.

Русский

Если Tendsto f откомаппит (comap i (nhds b)) к nhds c, то di.extend f b = c.

LaTeX

$$$\\text{Tendsto } f (\\operatorname{comap} i (\\mathcal{N} b)) (\\mathcal{N} c) \\Rightarrow di.extend f b = c$$$

Lean4

theorem extend_eq_of_tendsto [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ}
    (hf : Tendsto f (comap i (𝓝 b)) (𝓝 c)) : di.extend f b = c :=
  haveI := di.comap_nhds_neBot
  hf.limUnder_eq

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