extend_symm_apply — Mathlib

English

For any γ, the symmetric path γ.symm extended at t equals the original path γ extended at 1 − t.

Русский

Для любого γ симметричный путь γ.symm, продолжение в точке t равно продолжению γ в точке 1 − t.

LaTeX

$$$\gamma^{\mathrm{symm}}.\mathrm{extend}(t) = \gamma.\mathrm{extend}(1 - t)$$$

Lean4

theorem extend_symm_apply (γ : Path x y) (t : ℝ) : γ.symm.extend t = γ.extend (1 - t) :=
  congrArg γ <| symm_projIcc _

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