mem_idealOfSet — Mathlib

English

Let s ⊆ X and f ∈ C(X,R). Then f ∈ idealOfSet(R,s) iff ∀ x ∈ s^c, f(x)=0.

Русский

Пусть s ⊆ X и f ∈ C(X,R). Тогда f ∈ idealOfSet(R,s) тогда и только тогда, когда ∀ x ∈ s^c, f(x)=0.

LaTeX

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

Lean4

theorem mem_idealOfSet {s : Set X} {f : C(X, R)} : f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0 := by
  convert Iff.rfl

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