coe_vanishingIdeal — Mathlib

English

The set-theoretic expression of vanishingIdeal via SetLike equality: the coe of vanishingIdeal t equals the predicate defining all f that vanish on t.

Русский

Пусть выражение vanishingIdeal через множество; равенство по присвоению: множество f, которые исчезают на t.

LaTeX

$$$\\\\forall t \\\\in \\Set(PrimeSpectrum(R)), \\\\operatorname{coe}(\\\\operatorname{vanishingIdeal}(t)) = \\{ f \\\\mid \\\\forall x \\\\in t, f \\\\in x.asIdeal \}$$$

Lean4

theorem coe_vanishingIdeal (t : Set (PrimeSpectrum R)) :
    (vanishingIdeal t : Set R) = {f : R | ∀ x ∈ t, f ∈ x.asIdeal} :=
  by
  ext f
  rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]
  apply forall_congr'; intro x
  rw [Submodule.mem_iInf]

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