theorem
RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict
(𝕜 : Type u_1)
(E : Type u_2)
[RCLike 𝕜]
[PseudoEMetricSpace E]
{A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)}
:
Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ)
(Subalgebra.comap (BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯)
(Subalgebra.restrictScalars ℝ A.toSubalgebra)) = Subalgebra.comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
(Subalgebra.restrictScalars ℝ
(StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).toSubalgebra)
On a star subalgebra of bounded continuous functions, the operations "restrict scalars to ℝ" and "forget that a bounded continuous function is a bounded" commute.