zeroLocus_anti_mono — Mathlib

English

For a graded algebra, enlarging a set decreases its zero locus with respect to the grading structure.

Русский

Для градуированной алгебры увеличение множества уменьшает его нулевую локацию в контексте градуирования.

LaTeX

$$$\\zeroLocus 𝒜 (t) \\supseteq \\zeroLocus 𝒜 (s)$ whenever $s \\subseteq t$$$

Lean4

theorem zeroLocus_anti_mono {s t : Set A} (h : s ⊆ t) : zeroLocus 𝒜 t ⊆ zeroLocus 𝒜 s :=
  (gc_set _).monotone_l h

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