transReflReparamAux_mem_I — Mathlib

English

For any path p, p.trans refl x1 equals p reparam with transReflReparamAux.

Русский

Для любой траектории p, p.trans refl x1 эквивалентна перенормировке p через transReflReparamAux.

LaTeX

$$$ p.trans (Path.refl x_1) = p.reparam(\lambda t, ⟨transReflReparamAux t, \dots⟩) $$$

Lean4

theorem transReflReparamAux_mem_I (t : I) : transReflReparamAux t ∈ I :=
  by
  unfold transReflReparamAux
  split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

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