toGrothendieck_bot — Mathlib

English

The toGrothendieck construction sends the bottom (trivial) pretopology to the bottom (trivial) Grothendieck topology.

Русский

Конструкция toGrothendieck отображает тривиальную препотопологию в тривиальную топологию Гротендей.

LaTeX

$$$\\mathrm{toGrothendieck}(C)\\ cqbemptyset = \\bot$$$

Lean4

/-- The trivial pretopology induces the trivial Grothendieck topology. -/
theorem toGrothendieck_bot : toGrothendieck (C := C) ⊥ = ⊥ :=
  (gi C).gc.l_bot

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