continuous_extend — Mathlib

English

In a T3-space, if s is dense in α and f : s → β satisfies a natural Tendsto condition for every b, then the extension is continuous.

Русский

В пространстве T3 и при плотном s в α продолжение f вдоль s непрерывно.

LaTeX

$$$[T3Space β] (hs : Dense s) (hf : \\forall b, \\exists c, Tendsto f (comap (↑) (𝓝 b)) (𝓝 c)) : Continuous (hs.extend f)$$$

Lean4

theorem continuous_extend [T3Space β] (hs : Dense s) (hf : ∀ a : α, ∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) :
    Continuous (hs.extend f) :=
  hs.isDenseInducing_val.continuous_extend hf

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