notMem_idealOfSet — Mathlib

English

For a subset s ⊆ X and f ∈ C(X,R), f ∉ idealOfSet(R,s) iff there exists x ∈ s^c with f(x) ≠ 0.

Русский

Для подмножества s ⊆ X и f ∈ C(X,R), f ∉ idealOfSet(R,s) тогда же, когда существует x ∈ s^c такое, что f(x) ≠ 0.

LaTeX

$$$ f \\notin I_s \\iff \\exists x \\notin s:\\; f(x) \\neq 0 $, где $I_s = \\{ f : C(X,R) : \\forall x \\notin s, f(x)=0 \\}$$$

Lean4

theorem notMem_idealOfSet {s : Set X} {f : C(X, R)} : f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0 := by
  simp_rw [mem_idealOfSet]; push_neg; rfl

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