homMk_eq_iff_leftFractionRel — Mathlib

English

Let X,Y be objects and z1,z2 : W.LeftFraction X Y. Then homMk z1 = homMk z2 if and only if LeftFractionRel z1 z2.

Русский

Пусть X,Y — объекты, z1,z2 : W.LeftFraction X Y. Тогда homMk z1 = homMk z2 тогда и только тогда, когда LeftFractionRel z1 z2.

LaTeX

$$$\forall {C} [\text{Category } C] {W} [W.HasLeftCalculusOfFractions] {X Y} (z_1,z_2 : W.LeftFraction X Y),\\ homMk\,z_1 = homMk\,z_2 \\Leftrightarrow\ LeftFractionRel\,z_1\,z_2$$$

Lean4

theorem homMk_eq_iff_leftFractionRel {X Y : C} (z₁ z₂ : W.LeftFraction X Y) :
    homMk z₁ = homMk z₂ ↔ LeftFractionRel z₁ z₂ :=
  @Equivalence.quot_mk_eq_iff _ _ (equivalenceLeftFractionRel W X Y) _ _

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