zeroLocus_anti_mono — Mathlib

English

If A ⊆ B are sets of functions, then vanishing sets enlarge in the opposite direction under inclusion, reflecting anti-monotonicity of the vanishing ideal.

Русский

Если A ⊆ B — множества функций, то множества нулей противо-подчинены относительно включения, отражая антимонотонность vanishingIdeal.

LaTeX

$$$I \\le J \\Rightarrow \\mathrm{zeroLocus}\\ K(J) \\le \\mathrm{zeroLocus}\\ K(I).$$$

Lean4

theorem zeroLocus_anti_mono {I J : Ideal (MvPolynomial σ k)} (h : I ≤ J) : zeroLocus K J ≤ zeroLocus K I :=
  fun _ hx p hp => hx p <| h hp

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