eq_of_zag — Mathlib

English

A Zag in a discrete category implies equality of endpoints.

Русский

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

LaTeX

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

Lean4

/-- A Zag in a discrete category entails an equality of its extremities -/
theorem eq_of_zag (X) {a b : Discrete X} (h : Zag a b) : a.as = b.as :=
  h.elim (fun ⟨f⟩ ↦ Discrete.eq_of_hom f) (fun ⟨f⟩ ↦ (Discrete.eq_of_hom f).symm)

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