comp₀

Mathlib.CategoryTheory.Localization.CalculusOfFractions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.LeftFraction.comp₀

Lean4

/-- Auxiliary definition for the composition of left fractions. -/
@[simp]
def comp₀ [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
    (z₃ : W.LeftFraction z₁.Y' z₂.Y') : W.LeftFraction X Z :=
  mk (z₁.f ≫ z₃.f) (z₂.s ≫ z₃.s) (W.comp_mem _ _ z₂.hs z₃.hs)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru