continuous_uncurry_extend_of_continuous_family

English

If γ is a family of paths and its uncurry is continuous, then the map t ↦ (γ t).extend is continuous in t.

Русский

Если γ — семейство путей, и его раскрутка непрерывна, то t ↦ (γ t).extend непрерывно по t.

LaTeX

$$Continuous (fun t => (γ t).extend)$$

Lean4

@[continuity]
theorem continuous_uncurry_extend_of_continuous_family {ι : Type*} [TopologicalSpace ι] {a b : ι → X}
    (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun t => ⇑(γ t).extend :=
  by
  apply h.comp (continuous_id.prodMap continuous_projIcc)
  exact zero_le_one

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