English
Let a, b, c be points in a normed space, and ω a 2-variable linear operator-valued map. If ω is curve-integrable along the path from a to b and along the path from b to c, then ω is curve-integrable along the concatenation of these two paths from a to c.
Русский
Пусть a, b, c — точки в нормированном пространстве, и ω — отображение ω: E × E → F через линейные отображения. Если ω регулируемо интегрируется по кривой от a к b и по кривой от b к c, то ω регулируемо интегрируется по кривой, полученной конкатенацией этих двух кривых, от a к c.
LaTeX
$$$\\text{CurveIntegrable}(\omega, \\gamma_{ab}) \\wedge \\text{CurveIntegrable}(\\omega, \\gamma_{bc}) \\Rightarrow \\text{CurveIntegrable}(\\omega, \\gamma_{ab} \\text{ trans } \\gamma_{bc})$$$
Lean4
protected theorem trans (h₁ : CurveIntegrable ω γab) (h₂ : CurveIntegrable ω γbc) : CurveIntegrable ω (γab.trans γbc) :=
(h₁.intervalIntegrable_curveIntegralFun_trans_left γbc).trans (h₂.intervalIntegrable_curveIntegralFun_trans_right γab)
