setOfIdeal — Mathlib

English

For I an ideal of C(X,R), the set setOfIdeal(I) consists of points x ∈ X such that not all f ∈ I vanish at x; equivalently, setOfIdeal(I) = { x ∈ X | ∀ f ∈ I, f(x)=0 }^c.

Русский

Для идеала I подпорядка C(X,R) множество setOfIdeal(I) состоит из точек x, где не все функции из I исчезают в x; эквивалентно: setOfIdeal(I) = {x : X | ∀ f ∈ I, f(x)=0}^c.

LaTeX

$$$ setOfIdeal(I) = \\{ x \\in X : \\forall f \\in I, f(x)=0 \\}^c $$$

Lean4

/-- Given an ideal `I` of `C(X, R)`, construct the set of points for which every function in the
ideal vanishes on the complement. -/
def setOfIdeal (I : Ideal C(X, R)) : Set X :=
  {x : X | ∀ f ∈ I, (f : C(X, R)) x = 0}ᶜ

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