English
A variant of the half-interval law giving another equivalent expression for the concatenated path in terms of the second segment.
Русский
Вариант закона через середину, дающий эквивалентное выражение для объединённого пути через вторую часть.
LaTeX
$$$ \\operatorname{curveIntegralFun}(\\omega, γ_{ab}.trans γ_{bc}, t) = 2 \\cdot \\operatorname{curveIntegralFun}(\\omega, γ_{bc}, 2t-1) $ for t in appropriate interval$$
Lean4
theorem curveIntegralFun_trans_of_half_lt (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) (ht₀ : 1 / 2 < t) :
curveIntegralFun ω (γab.trans γbc) t = (2 : ℕ) • curveIntegralFun ω γbc (2 * t - 1) :=
by
rw [← (γab.trans γbc).symm_symm, curveIntegralFun_symm_apply, Path.trans_symm,
curveIntegralFun_trans_of_lt_half (ht := by linarith), curveIntegralFun_symm_apply, smul_neg, neg_neg]
congr 2
ring