equivalenceLeftFractionRel — Mathlib

English

For any X, Y, the relation LeftFractionRel gives an equivalence relation on the set of LeftFractions: reflexive, symmetric, and transitive.

Русский

Для любых X, Y отношение LeftFractionRel образует эквивалентность на множестве LeftFraction: рефлексивность, симметричность и транзитивность.

LaTeX

$$@Equivalence (W.LeftFraction X Y) LeftFractionRel$$

Lean4

theorem equivalenceLeftFractionRel [W.HasLeftCalculusOfFractions] (X Y : C) :
    @_root_.Equivalence (W.LeftFraction X Y) LeftFractionRel
    where
  refl := LeftFractionRel.refl
  symm := LeftFractionRel.symm
  trans := LeftFractionRel.trans

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