zeroLocus_bot — Mathlib

English

Let 𝒜 be a grading of A. The vanishing locus of the bottom ideal is the entire space.

Русский

Пусть 𝒜 задаёт градацию на A. Нулевая локализация нижнего идеала равна всей области.

LaTeX

$$$ \operatorname{zeroLocus} 𝒜 ((\bot : \mathrm{Ideal}\, A) : \mathrm{Set}\, A) = \mathrm{Set.univ}$$$

Lean4

theorem zeroLocus_bot : zeroLocus 𝒜 ((⊥ : Ideal A) : Set A) = Set.univ :=
  (gc_ideal 𝒜).l_bot

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