English
Let i : α → β be a dense inducing map. If g : β → γ is such that ∀ᶠ x in comap i (𝓝 b), g(i x) = f x, and g is continuous at b, then extend f evaluated at b equals g(b).
Русский
Пусть i : α → β — плотное индуцирующее отображение. Если функция g : β → γ удовлетворяет условию, что по окружности comap i (𝓝 b) вдоль i(x) почти всегда выполняется g(i(x)) = f(x), и g непрерывна в b, то значение extend f в b равно g(b).
LaTeX
$$$\\\\forall b \\\\in \u03b2, \\\\Big( (\\\\forallᶠ x \\\\in \\,\\\\mathrm{comap}\\ i\\ (\\\\mathcal{N} b),\\\\ g(i x) = f x) \\\\land \\\\text{ContinuousAt } g b \Big) \Rightarrow \\\\(\\\\operatorname{extend} f\\\\, b) = g b$$$
Lean4
theorem extend_unique_at [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i)
(hf : ∀ᶠ x in comap i (𝓝 b), g (i x) = f x) (hg : ContinuousAt g b) : di.extend f b = g b :=
by
refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_
suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
clear hf f
refine eventually_comap.2 ((hg.eventually hs).mono ?_)
rintro _ hxs x rfl
exact hxs
