ext' — Mathlib

English

To show two paths are equal it suffices to prove they have identical edges, i.e., if for every i the i-th edges coincide, then the paths are equal.

Русский

Чтобы доказать равенство двух путей, достаточно показать совпадение их ребер: если для каждого i стрелка f.arrow i = g.arrow i, то f = g.

LaTeX

$$$\forall i,\ (f.arrow i = g.arrow i) \Rightarrow f = g$$$

Lean4

/-- To show two paths equal it suffices to show that they have the same edges. -/
@[ext]
theorem ext' {f g : Path X (n + 1)} (h : ∀ i, f.arrow i = g.arrow i) : f = g :=
  Truncated.Path.ext' h

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