Theorems · Theorem · general topology

Subalgebra.SeparatesPoints.rclike_to_real

∀ {𝕜 : Type u_1} {X : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] {A : StarSubalgebra 𝕜 C(X, 𝕜)},
  A.SeparatesPoints →
    (Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯)
        (Subalgebra.restrictScalars ℝ A.toSubalgebra)).SeparatesPoints

If a star subalgebra of C(X, 𝕜) separates points, then the real subalgebra of its purely real-valued elements also separates points.

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpace