iSup_basicOpen_eq_top_iff' — Mathlib

English

For a subset s of R, the supremum over all i in s of the basic opens D(i) equals the whole spectrum if and only if the ideal generated by s is the unit ideal.

Русский

Для подмножества s ⊆ R максимальная верхняя граница по открытым D(i) (i∈s) равна всему спектру тогда и только тогда порождающее s множество единичного идеала.

LaTeX

$$$$ \bigvee_{i \in s} \mathrm{basicOpen}(i) = \top \quad\Longleftrightarrow\quad \operatorname{span}(s) = \top. $$$$

Lean4

theorem iSup_basicOpen_eq_top_iff' {s : Set R} : (⨆ i ∈ s, PrimeSpectrum.basicOpen i) = ⊤ ↔ Ideal.span s = ⊤ :=
  by
  conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]
  simp

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