pathExtend — Mathlib

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γ

Похожие утверждения