isPullback_iff — Mathlib

English

For a square sq, sq.IsPullback holds if and only if sq.pullbackCone is an IsLimit (i.e., there exists a universal cone).

Русский

Для квадрата sq, sq.IsPullback эквивално тому, что sq.pullbackCone является IsLimit (существует универсальный конус).

LaTeX

$$sq.IsPullback ↔ Nonempty (IsLimit sq.pullbackCone)$$

Lean4

theorem isPullback_iff : sq.IsPullback ↔ Nonempty (IsLimit sq.pullbackCone) :=
  ⟨fun h ↦ ⟨h.isLimit⟩, fun h ↦ { w := sq.fac, isLimit' := h }⟩

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