English
Let J1 and J2 be Grothendieck topologies on a category C. If the families of sieves assigned by J1 and J2 agree at every object, i.e., for all X, J1.sieves(X) = J2.sieves(X), then J1 = J2.
Русский
Пусть J1 и J2 — топологии Гротендик на категорию C. Если для каждого объекта X множество решёт Sieves, задаваемое J1 на X, совпадает с аналогичным множеством для J2, то J1 = J2.
LaTeX
$$$J_1 = J_2 \quad\text{iff}\quad \forall X,\; J_1(X) = J_2(X).$$$
Lean4
/-- An extensionality lemma in terms of the coercion to a pi-type.
We prove this explicitly rather than deriving it so that it is in terms of the coercion rather than
the projection `.sieves`.
-/
@[ext]
theorem ext {J₁ J₂ : GrothendieckTopology C} (h : (J₁ : ∀ X : C, Set (Sieve X)) = J₂) : J₁ = J₂ :=
DFunLike.coe_injective h
