le_def — Mathlib

English

The order relation between Grothendieck topologies is defined pointwise: J1 ≤ J2 if and only if J1.X ⊆ J2.X for all objects X.

Русский

Положение между топологиями определяется по каждому объекту: J1 ≤ J2 тогда, когда J1(X) ⊆ J2(X) для всех X.

LaTeX

$$J1 ≤ J2 ↔ (J1 : ∀ X, Set (Sieve X)) ≤ J2$$

Lean4

theorem le_def {J₁ J₂ : GrothendieckTopology C} : J₁ ≤ J₂ ↔ (J₁ : ∀ X : C, Set (Sieve X)) ≤ J₂ :=
  Iff.rfl

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