toList_inj — Mathlib

English

For any p,q : Path a b, p.toList = q.toList if and only if p = q, under the same subsingleton assumption on arrows.

Русский

Для любых путей p,q: Path a b выполняется p.toList = q.toList тогда и только тогда, когда p = q, при условии существования подсинглтона стрел.

LaTeX

$$$\\forall a,b\\, (p,q:\\ Path\\ a\\ b),\\ p.toList = q.toList \\iff p = q.$$$

Lean4

@[simp]
theorem toList_inj {p q : Path a b} : p.toList = q.toList ↔ p = q :=
  (toList_injective _ _).eq_iff

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