pathExtend — Mathlib

English

If γ is a family of paths and g is continuous at y, then the map i ↦ (γ i).extend (g i) is continuous at y.

Русский

Если γ — семейство путей, а g непрерывна в точке y, то отображение i ↦ (γ i).extend (g i) непрерывно в y.

LaTeX

$$$\\text{ContinuousAt}( (\\lambda i. (\\gamma i).extend (g i)) , y) $$$

Lean4

theorem _root_.ContinuousAt.pathExtend {g : Y → ℝ} {l r : Y → X} (γ : ∀ y, Path (l y) (r y)) {y : Y}
    (hγ : ContinuousAt ↿γ (y, projIcc 0 1 zero_le_one (g y))) (hg : ContinuousAt g y) :
    ContinuousAt (fun i => (γ i).extend (g i)) y :=
  hγ.IccExtend (fun x => γ x) hg

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