mk_surjective

Mathlib.CategoryTheory.Localization.CalculusOfFractions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective

Lean4

theorem mk_surjective {X Y : C} (f : Localization.Hom W X Y) : ∃ (z : W.LeftFraction X Y), f = mk z :=
  by
  obtain ⟨z⟩ := f
  exact ⟨z, rfl⟩

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

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

Разделы

Аффилиация

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