mem_idealOfSet_compl_singleton — Mathlib

English

For X,Y with Topological spaces and R a topological semiring, the pair (setOfIdeal, idealOfSet) forms a Galois connection between subsets of X and ideals of C(X,R).

Русский

Для X,Y с топологическими пространствами и R — топологическое полупрямое кольцо, пара (setOfIdeal, idealOfSet) образует галуазовую связь между подмножествами X и идеалами C(X,R).

LaTeX

$$$ \\text{GaloisConnection}(setOfIdeal, idealOfSet(R,\\cdot)) $$$

Lean4

@[simp]
theorem mem_idealOfSet_compl_singleton (x : X) (f : C(X, R)) : f ∈ idealOfSet R ({ x }ᶜ : Set X) ↔ f x = 0 := by
  simp only [mem_idealOfSet, compl_compl, Set.mem_singleton_iff, forall_eq]

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