presieveOfSections_surjective — Mathlib

English

The presieveOfSections map is surjective, i.e., every presieve on U arises as presieveOfSections U s for some set s of sections.

Русский

Функция presieveOfSections сюрьективна: каждый presieve на U получается как presieveOfSections U s для некоторого множества s секций.

LaTeX

$$$\mathrm{Function.Surjective}(\text{presieveOfSections } U)$$$

Lean4

theorem presieveOfSections_surjective {U : X.AffineZariskiSite} : Function.Surjective (presieveOfSections U) := fun _ ↦
  ⟨_, presieveOfSections_sectionsOfPresieve _⟩

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