transAssocReparamAux — Mathlib

English

An auxiliary time-reparameterization function is defined piecewise to witness associativity of path concatenation.

Русский

Введена вспомогательная переparametrизация времени, чтобы доказать ассоциативность конкатенации путей.

LaTeX

$$$$\\mathrm{transAssocReparamAux}(t)=\\begin{cases}2t,& 0 \\le t \\le \\tfrac{1}{4},\\\\[2mm] t+\\tfrac{1}{4},& \\tfrac{1}{4} < t \\le \\tfrac{1}{2},\\\\[2mm] \\tfrac{t+1}{2},& \\tfrac{1}{2} < t \\le 1.\\end{cases}$$$$

Lean4

/-- Auxiliary function for `trans_assoc_reparam`. -/
def transAssocReparamAux (t : I) : ℝ :=
  if (t : ℝ) ≤ 1 / 4 then 2 * t else if (t : ℝ) ≤ 1 / 2 then t + 1 / 4 else 1 / 2 * (t + 1)

Похожие утверждения