hasLimit_of_equalizer_and_product

English

There is a HasLimit for F provided by the equalizer and product data.

Русский

Существует предел для F, обеспечиваемый данными равноселителя и произведения.

LaTeX

$$$HasLimit\,F$$$

Lean4

/-- Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of
`F` exists.
(This assumes the existence of all equalizers, which is technically stronger than needed.)
-/
theorem hasLimit_of_equalizer_and_product (F : J ⥤ C) [HasLimit (Discrete.functor F.obj)]
    [HasLimit (Discrete.functor fun f : Σ p : J × J, p.1 ⟶ p.2 => F.obj f.1.2)] [HasEqualizers C] : HasLimit F :=
  HasLimit.mk (limitConeOfEqualizerAndProduct F)

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