The prime spectrum

Extensions of Mathlib's RingTheory/Spectrum/Prime/, where PrimeSpectrum and PrimeSpectrum.basicOpen are defined: finite products of basic opens in the lattice of opens, and the bridge from a unit-ideal generating family to an open-site cover. These results are about topological prime spectra and need no scheme structure.