extend_eq_at' — Mathlib

English

If Tendsto f (nhds a) (nhds c) for some c, then di.extend f (i a) = f a.

Русский

Если f стремится к c по nhds a, то продолжение на i(a) равно f(a).

LaTeX

$$$\\text{extend\_eq\_at'}(di)(f)(a)(c) : Tendsto f (\\mathcal{N} a) (\\mathcal{N} c) \\Rightarrow di.extend f (i a) = f a$$$

Lean4

theorem extend_eq_at' [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ) (hf : Tendsto f (𝓝 a) (𝓝 c)) :
    di.extend f (i a) = f a :=
  di.extend_eq_at (continuousAt_of_tendsto_nhds hf)

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