English
A technical lemma about membership of ofLine with respect to a function on I; its exact content is a structural refinement used in proofs about line-based paths.
Русский
Техническая лемма о принадлежности у Path.ofLine, используемая в доказательствах свойств путей, полученных по линии.
LaTeX
$$$\text{(technical lemma about ofLine membership, used in proofs)}$$$
Lean4
/-- Concatenation of two paths from `x` to `y` and from `y` to `z`, putting the first
path on `[0, 1/2]` and the second one on `[1/2, 1]`. -/
@[trans]
def trans (γ : Path x y) (γ' : Path y z) : Path x z
where
toFun := (fun t : ℝ => if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ (↑)
continuous_toFun := by
refine (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp continuous_subtype_val <;> fun_prop
source' := by simp
target' := by norm_num
