English
For a fixed θ and a path γ: X from x to y, delayReflRight(θ, γ) is the path t ↦ γ(qRight(t, θ)), giving a reparameterized version of γ.
Русский
Для фиксированной величины θ и пути γ: X→Y, delayReflRight(θ, γ) есть путь t ↦ γ(qRight(t, θ)), представляющий повторную параметризацию γ.
LaTeX
$$delayReflRight(θ, γ): I → X defined by (delayReflRight(θ, γ))(t) = γ(qRight(t, θ)).$$
Lean4
/-- This is the function analogous to the one on p. 475 of [serre1951], defining a homotopy from
the product path `γ ∧ e` to `γ`. -/
def delayReflRight (θ : I) (γ : Path x y) : Path x y
where
toFun t := γ (qRight (t, θ))
continuous_toFun := by fun_prop
source' := by rw [qRight_zero_left, γ.source]
target' := by rw [qRight_one_left, γ.target]
