Theorems · Definition · general topology

Subalgebra.SeparatesPoints

{α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → [inst_5 : IsTopologicalSemiring A] → Subalgebra R C(α, A) → Prop

A version of Set.SeparatesPoints for subalgebras of the continuous functions, used for stating the Stone-Weierstrass theorem.

Defined in

Mathlib.Topology.ContinuousMap.Algebra

Cited by

18 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommSemiringTopologicalSpaceSemiringAlgebraIsTopologicalSemiring