sup_vanishingIdeal_le — Mathlib

English

For t and t' subsets of PrimeSpectrum(R), the sup of their vanishing ideals is contained in the vanishing ideal of their intersection:

Русский

Для подмножеств t и t' PrimeSpectrum(R) верхняя граница (объединение) их ванishing ideals включена в ванishingIdeal пересечения:

LaTeX

$$$\\mathrm{vanishingIdeal}(t) \\sqcup \\mathrm{vanishingIdeal}(t') \\leq \\mathrm{vanishingIdeal}(t \\cap t').$$$

Lean4

theorem sup_vanishingIdeal_le (t t' : Set (PrimeSpectrum R)) :
    vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t') :=
  by
  intro r
  rw [Submodule.mem_sup, mem_vanishingIdeal]
  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
  rw [mem_vanishingIdeal] at hf hg
  apply Submodule.add_mem <;> solve_by_elim

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