isSheaf_of_isSheafUniqueGluing_types

English

If a presheaf has a unique gluing property in the Type-valued setting, then it satisfies the standard sheaf condition.

Русский

Если прешейф обладает уникальной слепкой в случае значений в типах, то он удовлетворяет обычному условию шейфов.

LaTeX

$$$$F.\IsSheaf\text{ if } F.\IsSheafUniqueGluing,$$$$

Lean4

/-- The usual sheaf condition can be obtained from the sheaf condition
in terms of unique gluings.
-/
theorem isSheaf_of_isSheafUniqueGluing_types (Fsh : F.IsSheafUniqueGluing) : F.IsSheaf :=
  (isSheaf_iff_isSheafUniqueGluing_types F).mpr Fsh

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