TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover

theorem TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Presheaf C X), F.IsSheaf ↔ F.IsSheafOpensLeCover

This theorem states that for any category `C`, any topological space `X`, and any presheaf `F` on `X` with values in `C`, `F` is a sheaf on the site of open subsets of `X` if and only if it satisfies the `IsSheafOpensLeCover` sheaf condition. The `IsSheafOpensLeCover` condition is not the official definition of sheaves on spaces, but it has the advantage that it does not require the category `C` to have products.

More concisely: A presheaf on a topological space is a sheaf if and only if it satisfies the `IsSheafOpensLeCover` condition in Lean 4. (No reference to Lean or category theory terminology is needed in the statement.)