Theorems · Definition · general topology

ContinuousMap.idealOfSet

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

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.

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

16 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSemiringTopologicalSpaceIsTopologicalSemiring