English
Let g be a map into M with images staying in the source of f. Then Tendsto of the composite f.extend I ∘ g along l equals Tendsto of g along l to the target y when y ∈ f.source. This expresses compatibility of extension with convergence along a filter.
Русский
Пусть g: A → M так, что g замирает в области f, тогда стремление композиции f.extend I ∘ g совпадает со стремлением g к точке y при y ∈ f.source.
LaTeX
$$$\\mathrm{Tendsto}(f^{\\mathrm{ext}} \\circ g)\\; l\\; (\\mathcal{N}(f^{\\mathrm{ext}}(y))) \\quad\\text{iff}\\quad \\mathrm{Tendsto}(g)\\; l\\; \\mathcal{N}(y)$, под условием стабильности $hg$ и $hy$.$$
Lean4
theorem tendsto_extend_comp_iff {α : Type*} {l : Filter α} {g : α → M} (hg : ∀ᶠ z in l, g z ∈ f.source) {y : M}
(hy : y ∈ f.source) : Tendsto (f.extend I ∘ g) l (𝓝 (f.extend I y)) ↔ Tendsto g l (𝓝 y) :=
by
refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.comp⟩
have := (f.continuousAt_extend_symm hy).tendsto.comp h
rw [extend_left_inv _ hy] at this
filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu
simpa only [(· ∘ ·), extend_left_inv _ hz, mem_preimage] using hzu
