op — Mathlib · SciLib

English

For X,Y in C and z1,z2 in W.RightFraction X Y, if z1 is related to z2 by RightFractionRel, then their opposites z1.op and z2.op are related by LeftFractionRel.

Русский

Пусть X,Y в C и z1,z2 в W.RightFraction X Y; если z1 связано z2RelationRight через RightFractionRel, то z1.op и z2.op связаны через LeftFractionRel.

LaTeX

$$$\forall X,Y, \forall z_1,z_2 \in W.RightFraction(X,Y):\; (RightFractionRel\; z_1\; z_2) \Rightarrow (LeftFractionRel\; z_1^{op}\; z_2^{op})$$$

Lean4

theorem op {X Y : C} {z₁ z₂ : W.RightFraction X Y} (h : RightFractionRel z₁ z₂) : LeftFractionRel 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⟩

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