Theorems · Theorem · general topology

ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero

∀ {𝕜 : Type u_2} {A : Type u_3} [inst : RCLike 𝕜] [inst_1 : NonUnitalSemiring A] [inst_2 : Star A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousMul A] [T2Space A] [inst_6 : DistribMulAction 𝕜 A]
  [SMulCommClass 𝕜 A A] {s : Set 𝕜} [inst_8 : Fact (0 ∈ s)] [CompactSpace ↑s] (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A)
  (a : A),
  a * φ (ContinuousMapZero.id s) = 0 →
    a * φ (star (ContinuousMapZero.id s)) = 0 → Continuous ⇑φ → ∀ (f : ContinuousMapZero (↑s) 𝕜), a * φ f = 0

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNonUnitalSemiringStarTopologicalSpaceSeparatelyContinuousMulT2SpaceDistribMulActionSMulCommClassFactCompactSpace