English
Let C be a category equipped with a Grothendieck topology. For any subset S of Grothendieck topologies on C, the infimum sInf(S) is the greatest lower bound of S in the lattice of Grothendieck topologies. Equivalently, sInf(S) is a lower bound for every topology in S, and any other lower bound K that is below all members of S satisfies K ≤ sInf(S).
Русский
Пусть C — категория с топологией Гротендик. Пусть S — множество топологий Гротендик на C. Инфимум sInf(S) является наибольшей нижней границей множества S в решетке топологий Гротендик. Иными словами, sInf(S) — нижняя граница всех топологий из S, и если K — любая другая нижняя граница, удовлетворяющая K ≤ J для всех J ∈ S, тогда K ≤ sInf(S).
LaTeX
$$$\left(\forall J \in s\,\, sInf(s) \le J\right) \land \left(\forall K\,\left(\forall J \in s\, K \le J\right) \Rightarrow K \le sInf(s)\right)$$
Lean4
@[stacks 00Z7]
theorem isGLB_sInf (s : Set (GrothendieckTopology C)) : IsGLB s (sInf s) :=
by
refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_
· rfl
· exact _root_.isGLB_sInf _
