isConstructible_toSet — Mathlib

English

For every constructible data S over R, the underlying set S.toSet is a constructible subset (in the Zariski topology) of Spec R.

Русский

Для каждого конструктивного набора данных над R соответствующее множество-toSet является конструктивным подмножеством спектра Спекр(R) в царианской топологии.

LaTeX

$$$\mathrm{IsConstructible}(S^{\mathrm{toSet}})$$$

Lean4

theorem isConstructible_toSet (S : ConstructibleSetData R) : IsConstructible S.toSet :=
  by
  refine .biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_
  · rw [← isConstructible_compl]
    exact (isRetrocompact_zeroLocus_compl (Set.finite_range _)).isConstructible (isClosed_zeroLocus _).isOpen_compl
  · rw [← isConstructible_compl]
    exact (isRetrocompact_zeroLocus_compl (Set.finite_singleton _)).isConstructible (isClosed_zeroLocus _).isOpen_compl

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