TopCat.Sheaf.pushforward_sheaf_of_sheaf

theorem TopCat.Sheaf.pushforward_sheaf_of_sheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {F : TopCat.Presheaf C X}, F.IsSheaf → (f _* F).IsSheaf

This theorem states that the pushforward of a sheaf by a continuous map results in a sheaf. More specifically, for any category `C`, and for any topological spaces `X` and `Y` in the category of topological spaces `TopCat`, if there is a morphism `f` from `X` to `Y`, and `F` is a `C`-valued presheaf on `X` that is a sheaf, then the pushforward of `F` by `f` is also a sheaf. Here, a "sheaf" is a tool in topology and algebraic geometry that systematically tracks locally defined data attached to the open sets of a topological space. Meanwhile, "pushforward" is a way of transforming sheaves along a continuous map between topological spaces.

More concisely: Given a continuous map `f` between topological spaces `X` and `Y`, and a `C`-valued presheaf `F` on `X` that is a sheaf, the pushforward `f_!*F` of `F` is also a sheaf on `Y`.