factorizationData

Mathlib.CategoryTheory.MorphismProperty.Factorization

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

Lean4

/-- A chosen term in `FactorizationData W₁ W₂` when `HasFactorization W₁ W₂` holds. -/
noncomputable def factorizationData [HasFactorization W₁ W₂] : FactorizationData W₁ W₂ := fun _ =>
  Nonempty.some (HasFactorization.nonempty_mapFactorizationData _)

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

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

Разделы

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

Аффилиация

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