basicOpen_pow — Mathlib

English

A basic open set equals the supremum of basic opens obtained by projecting f via GradedAlgebra.proj over all indices.

Русский

BasicOpen для f равен супремуми BasicOpen по всем проекциям f через GradedAlgebra.proj.

LaTeX

$$$\mathrm{basicOpen}_{\mathcal{A}}(f) = \bigvee_{i \in \mathbb{N}} \mathrm{basicOpen}_{\mathcal{A}}(\mathrm{GradedAlgebra.proj}_{\mathcal{A}}(i)\,f)$$$

Lean4

@[simp]
theorem basicOpen_pow (f : A) (n : ℕ) (hn : 0 < n) : basicOpen 𝒜 (f ^ n) = basicOpen 𝒜 f :=
  TopologicalSpace.Opens.ext <| by simpa using zeroLocus_singleton_pow 𝒜 f n hn

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