sectionsOfPresieve — Mathlib

English

For any presieve P on U, the presieveOfSections applied to sectionsOfPresieve(P) recovers P exactly.

Русский

Для любого presieve P на U пресиев OfSections, применённый к sectionsOfPresieve(P), восстанавливает P в точности.

LaTeX

$$$presieveOfSections\_U( sectionsOfPresieve\, P ) = P$$$

Lean4

/-- The set of sections associated to a presieve. -/
def sectionsOfPresieve {U : X.AffineZariskiSite} (P : Presieve U) : Set Γ(X, U.toOpens) :=
  {f | P (homOfLE (U.basicOpen_le f))}

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