Theorems · Theorem · general topology

ContinuousMap.AlgHom.closure_ker_inter

∀ {F : Type u_2} {S : Type u_3} {K : Type u_4} {A : Type u_5} [inst : CommRing K] [inst_1 : Ring A]
  [inst_2 : Algebra K A] [inst_3 : TopologicalSpace K] [T1Space K] [inst_5 : TopologicalSpace A] [ContinuousSub A]
  [ContinuousSMul K A] [inst_8 : FunLike F A K] [inst_9 : AlgHomClass F K A K] [inst_10 : SetLike S A] [OneMemClass S A]
  [AddSubgroupClass S A] [SMulMemClass S K A] (φ : F),
  Continuous ⇑φ → ∀ (s : S), closure (↑s ∩ ↑(RingHom.ker φ)) = closure ↑s ∩ ↑(RingHom.ker φ)

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebraTopologicalSpaceT1SpaceTopologicalSpaceContinuousSubContinuousSMulFunLikeAlgHomClassSetLikeOneMemClassAddSubgroupClassSMulMemClass