cases

Mathlib.CategoryTheory.Localization.CalculusOfFractions

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

Lean4

theorem cases (α : W.LeftFraction X Y) : ∃ (Y' : C) (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s), α = LeftFraction.mk f s hs :=
  ⟨_, _, _, _, rfl⟩

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

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

Разделы

Аффилиация

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