leftFractionRel_op_iff — Mathlib

English

For any z1,z2, LeftFractionRel z1.op z2.op holds if and only if RightFractionRel z1 z2 holds.

Русский

Для любых z1,z2: LeftFractionRel(z1.op,z2.op) эквивалентно RightFractionRel(z1,z2).

LaTeX

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

Lean4

theorem leftFractionRel_op_iff {X Y : C} (z₁ z₂ : W.RightFraction X Y) :
    LeftFractionRel z₁.op z₂.op ↔ RightFractionRel z₁ z₂ :=
  ⟨fun h => h.unop, fun h => h.op⟩

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