English
Under suitable convergence hypotheses, the family of extensions γ x .extend converges to l₂ in the target filter.
Русский
При подходящих предположениях сходимости, семейство расширений γ x .extend сходится к l₂ в заданном фильтре.
LaTeX
$$$\\text{Tendsto}(\\lambda x. (\\gamma x).extend) \\, (\\mathcal{N}y \\times\\mathcal{l}_1) \\to l_2$$$
Lean4
theorem _root_.Filter.Tendsto.pathExtend {l r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X}
{γ : ∀ y, Path (l y) (r y)} (hγ : Tendsto ↿γ (𝓝 y ×ˢ l₁.map (projIcc 0 1 zero_le_one)) l₂) :
Tendsto (↿fun x => ⇑(γ x).extend) (𝓝 y ×ˢ l₁) l₂ :=
Filter.Tendsto.IccExtend _ hγ