Theorems · Theorem · general topology

polynomialFunctions.starClosure_le_equalizer

∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] {A : Type u_2}
  [inst_3 : StarRing R] [inst_4 : ContinuousStar R] [inst_5 : Semiring A] [inst_6 : StarRing A] [inst_7 : Algebra R A]
  (s : Set R) (φ ψ : C(↑s, R) →⋆ₐ[R] A),
  φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
    (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceIsTopologicalSemiringStarRingContinuousStarSemiringStarRingAlgebra