basicOpen_mul — Mathlib

English

The family of basic opens { basicOpen(r) } forms a topological basis for the opens on PrimeSpectrum R.

Русский

Семейство базисных открытых множеств { basicOpen(r) } образует топологический базис открытых множеств спектра PrimeSpectrum(R).

LaTeX

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

Lean4

theorem basicOpen_mul (f g : R) : basicOpen (f * g) = basicOpen f ⊓ basicOpen g :=
  TopologicalSpace.Opens.ext <| by simp [zeroLocus_singleton_mul]

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