vanishingIdeal_anti_mono — Mathlib

English

If A ⊆ B are sets of functions, then vanishingIdeal k B ≤ vanishingIdeal k A, reflecting anti-monotonicity.

Русский

Если A ⊆ B — множества функций, то vanishingIdeal k B ≤ vanishingIdeal k A (анти-монотония).

LaTeX

$$$A \\le B \\Rightarrow \\mathrm{vanishingIdeal}(k,B) \\le \\mathrm{vanishingIdeal}(k,A).$$$

Lean4

theorem vanishingIdeal_anti_mono {A B : Set (σ → K)} (h : A ≤ B) : vanishingIdeal k B ≤ vanishingIdeal k A :=
  fun _ hp x hx => hp x <| h hx

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