Theorems · Theorem · general topology

WeakDual.CharacterSpace.continuousMapEval_apply_apply

∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : CommRing 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : Nontrivial 𝕜] [inst_5 : NoZeroDivisors 𝕜] (x : X) (f : C(X, 𝕜)),
  ((WeakDual.CharacterSpace.continuousMapEval X 𝕜) x) f = f x

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommRingTopologicalSpaceIsTopologicalRingNontrivialNoZeroDivisors