IsPushout

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Square.IsPushout

Lean4

/-- The condition that a commutative square is a pushout square. -/
protected def IsPushout : Prop :=
  IsPushout sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄

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

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

Разделы

Аффилиация

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