setOfIdeal_open — Mathlib

English

The set of points where every function in an ideal vanishes on the complement is open; i.e., setOfIdeal(I) is open for any ideal I, provided the codomain has suitable topological properties (e.g., T2Space).

Русский

Множество точек, в которых каждая функция из идеала исчезает на комплемент, открыто; то есть setOfIdeal(I) открыто при заданной топологии т. д.

LaTeX

$$$ \\text{IsOpen}(setOfIdeal(I)) $$$

Lean4

theorem setOfIdeal_open [T2Space R] (I : Ideal C(X, R)) : IsOpen (setOfIdeal I) :=
  by
  simp only [setOfIdeal, Set.setOf_forall, isOpen_compl_iff]
  exact isClosed_iInter fun f => isClosed_iInter fun _ => isClosed_eq (map_continuous f) continuous_const

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