refl_trans_refl — Mathlib

English

The concatenation of a constant path with itself is again the constant path at that point.

Русский

Сцепление константного пути с самим собой снова дает константный путь в этой точке.

LaTeX

$$$ (\mathrm{Path.refl}\ a).\text{trans} (\mathrm{Path.refl}\ a) = \mathrm{Path.refl}\ a $$$

Lean4

@[simp]
theorem refl_trans_refl {a : X} : (Path.refl a).trans (Path.refl a) = Path.refl a :=
  by
  ext
  simp [Path.trans]

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