isConstructible_basicOpen — Mathlib

English

A basic open subset of Spec(R) is constructible in the spectral topology; in particular, basicOpen f is constructible for any f ∈ R.

Русский

Базовое открытое множество в спектре Spec(R) конструктивно; в частности, базовое открытое D(f) конструктивно для любого f.

LaTeX

$$$$ \operatorname{IsConstructible}( \operatorname{basicOpen}(f) ) $$$$

Lean4

theorem isConstructible_basicOpen {f : R} : IsConstructible (basicOpen f : Set (PrimeSpectrum R)) :=
  isRetrocompact_basicOpen.isConstructible (basicOpen f).2

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