CategoryTheory.Pretopology.toGrothendieck_bot

theorem CategoryTheory.Pretopology.toGrothendieck_bot : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Pretopology.toGrothendieck C ⊥ = ⊥

This theorem states that for any category `C` that has pullbacks, applying the function `CategoryTheory.Pretopology.toGrothendieck` to `C` and the trivial pretopology (denoted by `⊥`), yields the trivial Grothendieck topology (also denoted by `⊥`). In other words, the trivial pretopology on a given category induces the trivial Grothendieck topology on that category when we use the function `CategoryTheory.Pretopology.toGrothendieck`.

More concisely: The trivial pretopology in a category with pullbacks induces the trivial Grothendieck topology via the `CategoryTheory.Pretopology.toGrothendieck` function.