eq_reverse_iff — Mathlib

English

For arrows f: a → b and g: b → a, f = reverse(g) if and only if reverse(f) = g.

Русский

Для стрелок f: a → b и g: b → a выполняется: f = reverse(g) тогда и только тогда, когда reverse(f) = g.

LaTeX

$$$ \\forall f : a \\to b, g : b \\to a,\\quad f = \\mathrm{reverse}(g) \\;\\iff\\; \\mathrm{reverse}(f) = g $$$

Lean4

theorem eq_reverse_iff [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) (g : b ⟶ a) : f = reverse g ↔ reverse f = g :=
  by rw [← reverse_inj, reverse_reverse]

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