idealOfSet_closed — Mathlib

English

If R is a T2-space, then for any s ⊆ X the set of maps vanishing off s is closed in the function space C(X,R).

Русский

Пусть R имеет T2-пространство, тогда множество отображений, исчезающих вне s, закрыто в пространстве функций C(X,R).

LaTeX

$$$ [\\text{T2Space } R] \\Rightarrow \\text{IsClosed}( I_s ) \\text{ where } I_s = \\{ f ∈ C(X,R) : ∀ x ∉ s, f(x)=0 \\} $$$

Lean4

theorem idealOfSet_closed [T2Space R] (s : Set X) : IsClosed (idealOfSet R s : Set C(X, R)) :=
  by
  simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]
  exact isClosed_iInter fun x => isClosed_iInter fun _ => isClosed_eq (continuous_eval_const x) continuous_const

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