eq_biUnion_of_isOpen — Mathlib

English

The collection of all basicOpen(r) forms a topological basis for opens on PrimeSpectrum.

Русский

Коллекция всех basicOpen(r) образует топологический базис для открытых множеств спектра.

LaTeX

$$$$ \\text{IsTopologicalBasis}( \\{ \\mathrm{basicOpen}(r) : r \\in R \\} ). $$$$

Lean4

theorem eq_biUnion_of_isOpen {s : Set (PrimeSpectrum R)} (hs : IsOpen s) :
    s = ⋃ (r : R) (_ : ↑(basicOpen r) ⊆ s), basicOpen r :=
  (isTopologicalBasis_basic_opens.open_eq_sUnion' hs).trans <| by aesop

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