symm — Mathlib

English

The reverse of a path γ from x to y is a path γ^{symm} from y to x, defined by (γ^{symm})(t) = γ(σ(t)) with σ(t) = 1 − t.

Русский

Обратная/path γ^{symm} пути γ из x в y — путь из y в x и задаётся (γ^{symm})(t) = γ(1−t).

LaTeX

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

Lean4

/-- The reverse of a path from `x` to `y`, as a path from `y` to `x` -/
@[symm, simps]
def symm (γ : Path x y) : Path y x where
  toFun := γ ∘ σ
  continuous_toFun := by fun_prop
  source' := by simp
  target' := by simp

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