toSet — Mathlib

English

The toSet construction selects the constructible subset defined by the data (g, f) as zero-loci difference V(g) \\ V(f).

Русский

toSet описывает конструктивное множество как разность нулевых локаций V(g) \\ V(f).

LaTeX

$$toSet (C) = zeroLocus (Set.range C.g) \\ zeroLocus { C.f }$$

Lean4

/-- Given the data of a basic constructible set `s`, namely a tuple `(f, g₁, ..., gₙ)` such that
`s = V(g₁, ..., gₙ) \ V(f)`, return `s`. -/
def toSet (C : BasicConstructibleSetData R) : Set (PrimeSpectrum R) :=
  zeroLocus (Set.range C.g) \ zeroLocus { C.f }

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