English
Let i : α → β be a dense inducing map in a T3-space setting. If for a given b ∈ β there is a tail condition hf ensuring Tendsto f along comap i (𝓝 x) to some nhds, then di.extend f is continuous at b.
Русский
Пусть i : α → β — плотное индуцирующее отображение в пространстве T3. Если для некоторого b ∈ β существует условие hf, гарантирующее, что Tendsto f по направлению comap i (𝓝 x) к 𝓝 c, то di.extend f непрерывно в b.
LaTeX
$$$\\\\forall b, \\\\Big( \\\\forall V' \\\\in \\\\mathcal{N}(\\\\mathrm{extend} f (b)), \\\\text{IsClosed } V' \\\\Rightarrow \\\\ldots \Big) \\\\Rightarrow \\\\text{ContinuousAt } (\\\\mathrm{extend} f) b$$$
Lean4
theorem continuousAt_extend [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i)
(hf : ∀ᶠ x in 𝓝 b, ∃ c, Tendsto f (comap i <| 𝓝 x) (𝓝 c)) : ContinuousAt (di.extend f) b :=
by
set φ := di.extend f
haveI := di.comap_nhds_neBot
suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
intro V' V'_in V'_closed
set V₁ := {x | Tendsto f (comap i <| 𝓝 x) (𝓝 <| φ x)}
have V₁_in : V₁ ∈ 𝓝 b := by
filter_upwards [hf]
rintro x ⟨c, hc⟩
rwa [← di.extend_eq_of_tendsto hc] at hc
obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by
simpa [and_assoc] using
((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
rintro x ⟨x_in₁, x_in₂⟩
have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
apply V'_closed.mem_of_tendsto x_in₁
use V₂
tauto
