English
If f: Y → Path x y and g: Y → Path y z are continuous, then t ↦ (f(t)).trans (g(t)) is continuous.
Русский
Если f: Y → Path(x,y) и g: Y → Path(y,z) непрерывны, то t ↦ (f(t)).trans(g(t)) непрерывно.
LaTeX
$$Continuous f, Continuous g ⇒ Continuous (t ↦ (f t).trans (g t))$$
Lean4
@[continuity]
theorem trans_continuous_family {ι : Type*} [TopologicalSpace ι] {a b c : ι → X} (γ₁ : ∀ t : ι, Path (a t) (b t))
(h₁ : Continuous ↿γ₁) (γ₂ : ∀ t : ι, Path (b t) (c t)) (h₂ : Continuous ↿γ₂) :
Continuous ↿fun t => (γ₁ t).trans (γ₂ t) :=
by
have h₁' := Path.continuous_uncurry_extend_of_continuous_family γ₁ h₁
have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂
simp only [HasUncurry.uncurry, Path.trans]
refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_
· change Continuous ((fun p : ι × ℝ => (γ₁ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x : I → ℝ))
exact h₁'.comp (continuous_id.prodMap <| continuous_const.mul continuous_subtype_val)
· change Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))
exact h₂'.comp (continuous_id.prodMap <| (continuous_const.mul continuous_subtype_val).sub continuous_const)
· rintro st hst
simp [hst]
