basicOpen_mul — Mathlib

English

The basic open set respects multiplication: basicOpen 𝒜(fg) equals the intersection of basicOpen 𝒜 f and basicOpen 𝒜 g.

Русский

BasicOpen сохраняет умножение: basicOpen 𝒜(fg) равно пересечению basicOpen 𝒜 f и basicOpen 𝒜 g.

LaTeX

$$$\mathrm{basicOpen}_{\mathcal{A}}(f\,g) = \mathrm{basicOpen}_{\mathcal{A}}(f) \cap \mathrm{basicOpen}_{\mathcal{A}}(g)$$$

Lean4

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

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