mem_setOfIdeal — Mathlib

English

For any ideal I and any x ∈ X, x ∈ setOfIdeal(I) iff there exists a function f ∈ I with f(x) ≠ 0.

Русский

Для любого идеала I и любой точки x ∈ X верно: x ∈ setOfIdeal(I) тогда и только тогда, когда существует f ∈ I такое, что f(x) ≠ 0.

LaTeX

$$$ x \\in setOfIdeal(I) \\iff \\exists f \\in I,\\; f(x) \\neq 0 $$$

Lean4

theorem mem_setOfIdeal {I : Ideal C(X, R)} {x : X} : x ∈ setOfIdeal I ↔ ∃ f ∈ I, (f : C(X, R)) x ≠ 0 := by
  simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_setOf]; push_neg; rfl

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