tendsto_extend — Mathlib

English

If f is continuous at a, then f tends to the extended value at i(a): Tendsto f (nhds a) (nhds (di.extend f (i a))).

Русский

Если f непрерывна в точке a, то f стремится к продолжающемуся значению в i(a).

LaTeX

$$$\\text{tendsto_extend }(di)(f) : \\operatorname{Tendsto} f (\\mathcal{N} a) (\\mathcal{N}(di.extend f (i a)))$$$

Lean4

theorem tendsto_extend (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
    Tendsto f (𝓝 a) (𝓝 (di.extend f (i a))) :=
  by
  rw [IsDenseInducing.extend, ← di.nhds_eq_comap]
  exact tendsto_nhds_limUnder ⟨_, hf⟩

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