English
Let X be a scheme and s a sieve on X. Then s belongs to jointlySurjectiveTopology X iff s is covered by the jointlySurjectivePretopology on X.
Русский
Пусть X — схема, и s — сит в X. Тогда s принадлежит jointlySurjectiveTopology X тогда, когда s покрывается jointlySurjectivePretopology на X.
LaTeX
$$$s \\in jointlySurjectiveTopology X \\iff s \\in jointlySurjectivePretopology X$$$
Lean4
theorem mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology {X : Scheme.{u}} {s : Sieve X} :
s ∈ jointlySurjectiveTopology X ↔ jointlySurjectivePretopology X ↑s :=
Iff.rfl
