extend_eq_of_tendsto — Mathlib

English

Let hs be a dense set. If f : s → β is such that Tendsto f (comap Subtype.val (nhds a)) (nhds b), then hs.extend f a = b.

Русский

Пусть hs плотна. Если f : s → β удовлетворяет Tendsto f (comap Subtype.val (nhds a)) (nhds b), то hs.extend f a = b.

LaTeX

$$$[T2Space \\beta] (hs : Dense s) \\\\{a: \\alpha\\}\\\\{b: β\\\\} (hf: Tendsto f (\\\\mathrm{comap} (\\\\iota) (\\\\mathcal{N} a)) (\\\\mathcal{N} b)) : \\\\; hs.extend f a = b$$$

Lean4

theorem extend_eq_of_tendsto [T2Space β] (hs : Dense s) {a : α} {b : β} (hf : Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) :
    hs.extend f a = b :=
  hs.isDenseInducing_val.extend_eq_of_tendsto hf

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