op — Mathlib · SciLib

English

Taking opposites converts LeftFractionRel to RightFractionRel: if z1,z2 are related by LeftFractionRel, then z1.op,z2.op are related by RightFractionRel.

Русский

Преобразование через опозитLeftFractionRel преобразует к RightFractionRel: если z1,z2 связаны отношением LeftFractionRel, то z1.op,z2.op связаны RightFractionRel.

LaTeX

$$$LeftFractionRel(z_1,z_2) \Rightarrow RightFractionRel(z_1^{op}, z_2^{op})$$$

Lean4

theorem op {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : LeftFractionRel z₁ z₂) : RightFractionRel z₁.op z₂.op :=
  by
  obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
  exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs, Quiver.Hom.unop_inj hf, ht⟩

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