exists_rightFraction — Mathlib

English

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

Русский

Если в наличии правый калькулус дробей, то для любой LeftFraction φ существует 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_rightFraction [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) :
    ∃ (ψ : W.RightFraction X Y), ψ.s ≫ φ.f = ψ.f ≫ φ.s :=
  HasRightCalculusOfFractions.exists_rightFraction φ

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