reflTrans — Mathlib

English

Let X be a topological space and p a path from x0 to x1. The concatenation of the constant path at x0 with p is homotopic to p.

Русский

Пусть X — топологическое пространство, и p — путь от x0 до x1. Конкатенация константного пути в x0 с p гомотопна к p.

LaTeX

$$$$(c_{x_0} \\star p) \\sim p$$$$

Lean4

/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from `(Path.refl x₀).trans p` to `p`. -/
def reflTrans (p : Path x₀ x₁) : Homotopy ((Path.refl x₀).trans p) p :=
  (transRefl p.symm).symm₂.cast (by simp) (by simp)

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