Theorems · Theorem · general topology

ContinuousMapZero.elemental_eq_top

∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : Fact (0 ∈ s)] [inst_2 : CompactSpace ↑s],
  NonUnitalStarAlgebra.elemental 𝕜 (ContinuousMapZero.id s) = ⊤

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeFactCompactSpace