exists_leftFraction — Mathlib

English

If W.HasRightCalculusOfFractions, then for any φ: W.LeftFraction X Y there exists ψ: W.RightFraction X Y such that ψ.s ≫ φ.f = ψ.f ≫ φ.s.

Русский

Если выполнен правый калькулус дробей, то для любой φ: W.LeftFraction X Y есть ψ: W.RightFraction X Y, удовлетворяющее ψ.s ≫ φ.f = ψ.f ≫ φ.s.

LaTeX

$$$\exists \psi : W.RightFraction X Y, \ \psi.s \circ φ.f = \psi.f \circ φ.s$$$

Lean4

theorem exists_leftFraction [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) :
    ∃ (ψ : W.LeftFraction X Y), φ.f ≫ ψ.s = φ.s ≫ ψ.f :=
  HasLeftCalculusOfFractions.exists_leftFraction φ

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