instPreservesFiniteProductsOppositeLightProfiniteVal

English

Each LightCondensed object X preserves finite products: the associated functor X.val preserves all finite products.

Русский

Каждый LightCondensed объект X сохраняет конечные произведения: соответствующий функтор X.val сохраняет все конечные произведения.

LaTeX

$$$\text{PreservesFiniteProducts}(X.\mathrm{val})$$$

Lean4

/-- A light condensed object preserves finite products. -/
noncomputable instance (X : LightCondensed A) : PreservesFiniteProducts X.val :=
  isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.val |>.mp X.cond |>.1

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