instHasPullbacksPresieve₀OfHasPullbacks

English

If K has pullbacks, then for any E : ZeroHypercover X, f : Y → X, E.presieve₀.HasPullbacks f holds.

Русский

Если у K есть вытяжки, то для любого E: ZeroHypercover X и f: Y → X выполняется HasPullbacks у E.presieve₀ по f.

LaTeX

$$E.presieve₀.HasPullbacks f$$

Lean4

instance (K : Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) :
    E.presieve₀.HasPullbacks f :=
  K.hasPullbacks_of_mem _ E.mem₀

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