path_trans — Mathlib

English

Let f: Y → Path x y and g: Y → Path y z be continuous. Then the function 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, fun_prop]
theorem _root_.Continuous.path_trans {f : Y → Path x y} {g : Y → Path y z} :
    Continuous f → Continuous g → Continuous fun t => (f t).trans (g t) :=
  by
  intro hf hg
  apply continuous_uncurry_iff.mp
  exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

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