English
Concatenation of two GenLoops along the i-th coordinate: given i and two N-dimensional loops f,g, one obtains a new GenLoop that first follows f on the first half of the i-th coordinate and then switches to g on the second half, with a precise coordinate-wise stitching.
Русский
Объединение двух GenLoop вдоль i-й координаты: задано i и две петли f, g, образуется новая петля GenLoop, которая сначала следует по f на первой половине i-й координаты, затем переключается на g на второй половине, с точной поклейкой по координатам.
LaTeX
$$$\\mathrm{transAt}(i; f,g)\\;:\\; Ω^N X x\\to Ω^N X x$ равняется по кускам конкатенацией вдоль координаты $i$$$
Lean4
/-- Concatenation of two `GenLoop`s along the `i`th coordinate. -/
def transAt (i : N) (f g : Ω^ N X x) : Ω^ N X x :=
copy (fromLoop i <| (toLoop i f).trans <| toLoop i g)
(fun t =>
if (t i : ℝ) ≤ 1 / 2 then f (Function.update t i <| Set.projIcc 0 1 zero_le_one (2 * t i))
else g (Function.update t i <| Set.projIcc 0 1 zero_le_one (2 * t i - 1)))
(by
ext1; symm
dsimp only [Path.trans, fromLoop, Path.coe_mk_mk, Function.comp_apply, mk_apply, ContinuousMap.comp_apply,
ContinuousMap.coe_coe, funSplitAt_apply, ContinuousMap.uncurry_apply, ContinuousMap.coe_mk,
Function.uncurry_apply_pair]
split_ifs
· change f _ = _; congr 1
· change g _ = _; congr 1)
