trans_refl_reparam — Mathlib

English

For any t, transReflReparamAux t lies in I (unit interval).

Русский

Для любого t, transReflReparamAux t лежит в I (единичный интервал).

LaTeX

$$$ transReflReparamAux(t) \in I $$$

Lean4

theorem trans_refl_reparam (p : Path x₀ x₁) :
    p.trans (Path.refl x₁) =
      p.reparam (fun t => ⟨transReflReparamAux t, transReflReparamAux_mem_I t⟩) (by fun_prop)
        (Subtype.ext transReflReparamAux_zero) (Subtype.ext transReflReparamAux_one) :=
  by
  ext
  unfold transReflReparamAux
  simp only [Path.trans_apply, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]
  split_ifs
  · rfl
  · rfl
  · simp
  · simp

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