reverse_inj — Mathlib

English

Reverse is injective on arrows: if reverse f = reverse g then f = g.

Русский

Обратное отображение инъективно на стрелках: если reverse f = reverse g, то f = g.

LaTeX

$$$ \\operatorname{reverse} f = \\operatorname{reverse} g \\;\\Longleftrightarrow\\; f = g $$$

Lean4

@[simp]
theorem reverse_inj [h : HasInvolutiveReverse V] {a b : V} (f g : a ⟶ b) : reverse f = reverse g ↔ f = g :=
  by
  constructor
  · rintro h
    simpa using congr_arg Quiver.reverse h
  · rintro h
    congr

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