English
If Y is Regular and B ⊆ closure A and for every x ∈ B f has a limit along nhdsWithin x A, then extendFrom A f is continuous on B.
Русский
Если Y достаточно регулярна и B ⊆ closure A, и для каждого x ∈ B существует предел функции f в nhdsWithin x A, то extendFrom A f непрерывна на B.
LaTeX
$$$$ B \\subseteq \\overline{A} \\Rightarrow (\\forall x \\in B, \\exists y, \\mathrm{Tendsto}\n f (\\mathcal{N}_A x) (\\mathcal{N} y)) \\Rightarrow \\mathrm{ContinuousOn}(\\mathrm{extendFrom}(A,f), B). $$$$
Lean4
/-- If `f` is a function to a T₃ space `Y` which has a limit within `A` at any
point of a set `B ⊆ closure A`, then `extendFrom A f` is continuous on `B`. -/
theorem continuousOn_extendFrom [RegularSpace Y] {f : X → Y} {A B : Set X} (hB : B ⊆ closure A)
(hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)) : ContinuousOn (extendFrom A f) B :=
by
set φ := extendFrom A f
intro x x_in
suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x by
simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
intro V' V'_in V'_closed
obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V' :=
by
have := tendsto_extendFrom (hf x x_in)
rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
suffices ∀ y ∈ V ∩ B, φ y ∈ V' from mem_of_superset (inter_mem_inf V_in <| mem_principal_self B) this
rintro y ⟨hyV, hyB⟩
haveI := mem_closure_iff_nhdsWithin_neBot.mp (hB hyB)
have limy : Tendsto f (𝓝[A] y) (𝓝 <| φ y) := tendsto_extendFrom (hf y hyB)
have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV
have : V ∩ A ∈ 𝓝[A] y := by simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
exact V'_closed.mem_of_tendsto limy (mem_of_superset this hV)
