lift₃

Mathlib.CategoryTheory.MorphismProperty.Representable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.relativelyRepresentable.lift₃

Lean4

/-- The lift obtained from the universal property of `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃)`. -/
noncomputable def lift₃ : Z ⟶ pullback₃ hf₁ f₂ f₃ :=
  pullback.lift (hf₁.lift' x₁ x₂ h₁₂) (hf₁.lift' x₁ x₃ h₁₃) (by simp)

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

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

Разделы

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

Аффилиация

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