hasFiniteWidePullbacks_of_hasFiniteLimits

English

If C has finite limits, then C has finite wide pullbacks.

Русский

Если в C существуют конечные пределы, то существуют конечные широкие вытяжки.

LaTeX

$$$\operatorname{HasFiniteLimits}(C) \Rightarrow \operatorname{HasFiniteWidePullbacks}(C)$$$

Lean4

/-- Finite wide pullbacks are finite limits, so if `C` has all finite limits,
it also has finite wide pullbacks
-/
instance (priority := 900) hasFiniteWidePullbacks_of_hasFiniteLimits [HasFiniteLimits C] : HasFiniteWidePullbacks C :=
  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteLimits.out _⟩

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