extend_symm — Mathlib

English

Equality of functions: the symmetric extension equals the extension composed with the map t ↦ 1 − t.

Русский

Равенство функций: продолжение симметричного пути равно продолжению пути после композиции с тождественным отображением t ↦ 1 − t.

LaTeX

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

Lean4

@[simp]
theorem extend_symm (γ : Path x y) : γ.symm.extend = (γ.extend <| 1 - ·) :=
  funext γ.extend_symm_apply

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