refl

Mathlib.CategoryTheory.Localization.CalculusOfFractions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.LeftFractionRel.refl

Lean4

theorem refl {X Y : C} (z : W.LeftFraction X Y) : LeftFractionRel z z :=
  ⟨z.Y', 𝟙 _, 𝟙 _, rfl, rfl, by simpa only [Category.comp_id] using z.hs⟩

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

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

Разделы

Аффилиация

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