English
In a T3-space setting, if i : α → β is dense and for every b ∈ β there exists c with Tendsto f along comap i (𝓝 b) to 𝓝 c, then the extension extend f : β → γ is continuous.
Русский
В пространстве T3, если i : α → β плотное и для каждого b ∈ β существует c, такой что Tendsto f вдоль comap i (𝓝 b) до 𝓝 c, тогда продолжение extend f непрерывно на β.
LaTeX
$$$\\\\forall b, \\\\exists c, \\\\ Tendsto f (\\\\mathrm{comap}\\ i (\\\\mathcal{N} b)) (\\\\mathcal{N} c) \\\\Rightarrow \\\\text{Continuous}(\\\\mathrm{extend} f)$$$
Lean4
theorem continuous_extend [T3Space γ] {f : α → γ} (di : IsDenseInducing i)
(hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) : Continuous (di.extend f) :=
continuous_iff_continuousAt.mpr fun _ => di.continuousAt_extend <| univ_mem' hf
