eq_of_zigzag — Mathlib

English

A Zigzag in a discrete category implies equality of endpoints.

Русский

Zigzag в дискретной категории означает равенство концов.

LaTeX

$$$\forall X\ {a,b : \mathrm{Discrete}(X)},\ Zigzag\ a b \Rightarrow a.as = b.as$$$

Lean4

/-- A zigzag in a discrete category entails an equality of its extremities -/
theorem eq_of_zigzag (X) {a b : Discrete X} (h : Zigzag a b) : a.as = b.as := by
  induction h with
  | refl => rfl
  | tail _ h eq =>
    exact
      eq.trans
        (eq_of_zag _ h)
          -- TODO: figure out the right way to generalise this to `Zigzag`.

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