instPreservesFiniteProductsOppositeStoneanVal

English

A condensed object regarded as a sheaf on Stonean preserves finite products

Русский

Конденсированный объект, рассматриваемый как sheaf на Stonean, сохраняет конечные произведения

LaTeX

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

Lean4

/-- A condensed object regarded as a sheaf on `Stonean` preserves finite products. -/
noncomputable instance (X : Sheaf (coherentTopology Stonean.{u}) A) : PreservesFiniteProducts X.val :=
  isSheaf_iff_preservesFiniteProducts_of_projective X.val |>.mp X.cond

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