English
Let i : α → β be dense inducing, and suppose for every b ∈ β there exists c ∈ γ with Tendsto f along comap i (𝓝 b) to 𝓝 c. Then for all a ∈ α, (extend f)(i(a)) = f(a).
Русский
Пусть i : α → β — плотное индуцирующее отображение, и предположим, что для каждого b ∈ β существует c ∈ γ such that f тянется к c по мере comap i (𝓝 b). Тогда для всех a ∈ α имеет место (extend f)(i(a)) = f(a).
LaTeX
$$$\\\\forall a \\\\in \u03b1, \\\\(\\\\operatorname{extend} f)(i(a)) = f(a) \\\\;,$$$
Lean4
/-- Variation of `extend_eq` where we ask that `f` has a limit along `comap i (𝓝 b)` for each
`b : β`. This is a strictly stronger assumption than continuity of `f`, but in a lot of cases
you'd have to prove it anyway to use `continuous_extend`, so this avoids doing the work twice. -/
theorem extend_eq' [T2Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c))
(a : α) : di.extend f (i a) = f a := by
rcases hf (i a) with ⟨b, hb⟩
refine di.extend_eq_at' b ?_
rwa [← di.isInducing.nhds_eq_comap] at hb
