isPullback_of_binaryFan_isLimit — Mathlib

English

If c is a binary fan on Y and Z and is a limit, then the induced square in Over X is a pullback.

Русский

Если c — бинарный фан над Y и Z и он является пределом, то получившийся квадрат в Over X является пуллбеком.

LaTeX

$$$\text{IsPullback} \; c.fst.left \; c.snd.left \; Y.hom \ Z.hom$$$

Lean4

theorem isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) :
    IsPullback c.fst.left c.snd.left Y.hom Z.hom :=
  ⟨by simp, ⟨hc.pullbackConeEquivBinaryFanInverse⟩⟩

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