Theorems · Definition · general topology

WeakDual.CharacterSpace.continuousMapEval

(X : Type u_1) →
  (𝕜 : Type u_2) →
    [inst : TopologicalSpace X] →
      [inst_1 : CommRing 𝕜] →
        [inst_2 : TopologicalSpace 𝕜] →
          [inst_3 : IsTopologicalRing 𝕜] →
            [Nontrivial 𝕜] → [NoZeroDivisors 𝕜] → C(X, ↑(WeakDual.characterSpace 𝕜 C(X, 𝕜)))

The natural continuous map from a locally compact topological space X to the WeakDual.characterSpace 𝕜 C(X, 𝕜) which sends x : X to point evaluation at x.

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommRingTopologicalSpaceIsTopologicalRingNontrivialNoZeroDivisors