Theorems · Definition · general topology

ContinuousMap.setOfIdeal

{X : Type u_1} →
  {R : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : Semiring R] → [inst_2 : TopologicalSpace R] → [inst_3 : IsTopologicalSemiring R] → Ideal C(X, R) → Set X

Given an ideal I of C(X, R), construct the set of points for which every function in the ideal vanishes on the complement.

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

12 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSemiringTopologicalSpaceIsTopologicalSemiring