English
For a topological ring R and a subset s ⊆ X, the set I_s := { f ∈ C(X,R) : ∀ x ∉ s, f(x)=0 } is an ideal in C(X,R).
Русский
Для топологической кольцевой функции R и подмножества s ⊆ X, множество I_s = { f ∈ C(X,R) : ∀ x ∉ s, f(x)=0 } образует идеал в C(X,R).
LaTeX
$$$ I_s = \\{ f \\in C(X,R) : \\forall x \\notin s,\\; f(x)=0 \\} \\text{ является идеалом в } C(X,R) $$$
Lean4
/-- Given a topological ring `R` and `s : Set X`, construct the ideal in `C(X, R)` of functions
which vanish on the complement of `s`. -/
def idealOfSet (s : Set X) : Ideal C(X, R)
where
carrier := {f : C(X, R) | ∀ x ∈ sᶜ, f x = 0}
add_mem' {f g} hf hg x hx := by simp [hf x hx, hg x hx, add_zero]
zero_mem' _ _ := rfl
smul_mem' c _ hf x hx := mul_zero (c x) ▸ congr_arg (fun y => c x * y) (hf x hx)
