IsPullback

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

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

Lean4

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

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

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

Разделы

Аффилиация

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