StoneWeierstrass

📁 Source: Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Statistics

Metric	Count
Definitions attachBound	1
Theorems closure_ker_inter, abs_mem_subalgebra_closure, adjoin_id_eq_span_one_add, adjoin_id_eq_span_one_union, algHom_ext_map_X, attachBound_apply_coe, comp_attachBound_mem_closure, continuousMap_mem_subalgebra_closure_of_separatesPoints, elemental_id_eq_top, exists_mem_subalgebra_near_continuousMap_of_separatesPoints, exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints, exists_mem_subalgebra_near_continuous_of_separatesPoints, induction_on, induction_on_of_compact, inf_mem_closed_subalgebra, inf_mem_subalgebra_closure, ker_evalStarAlgHom_eq_closure_adjoin_id, ker_evalStarAlgHom_inter_adjoin_id, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, polynomial_comp_attachBound, polynomial_comp_attachBound_mem, starAlgHom_ext_map_X, starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, subalgebra_topologicalClosure_eq_top_of_separatesPoints, sublattice_closure_eq_top, sup_mem_closed_subalgebra, sup_mem_subalgebra_closure, adjoin_id_dense, elemental_eq_top, induction_on, induction_on_of_compact, mul_nonUnitalStarAlgHom_apply_eq_zero, nonUnitalStarAlgHom_apply_mul_eq_zero, rclike_to_real, starClosure_topologicalClosure, topologicalClosure	36
Total	37

ContinuousMap

Definitions

Name	Category	Theorems
attachBound 📖	CompOp	4 math math: attachBound_apply_coe, comp_attachBound_mem_closure, polynomial_comp_attachBound, polynomial_comp_attachBound_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_mem_subalgebra_closure 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing abs instLatticeOfTopologicalLattice Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid instAddGroupOfIsTopologicalAddGroup Real.instAddGroup instIsTopologicalAddGroupReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.comp' continuous_abs Real.instIsOrderedAddMonoid instOrderTopologyReal continuous_induced_dom NonUnitalSeminormedRing.toIsTopologicalRing HasSolidNorm.toTopologicalLattice instHasSolidNormReal instIsTopologicalAddGroupReal comp_attachBound_mem_closure
adjoin_id_eq_span_one_add 📖	mathematical	—	SetLike.coe StarSubalgebra ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar algebra Algebra.id instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing StarSubalgebra.setLike StarAlgebra.adjoin Set.instSingletonSet restrict id Set.add instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd Submodule instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule.setLike Submodule.span instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NonUnitalStarSubalgebra instNonUnitalSemiringOfIsTopologicalSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin IsScalarTower.right Algebra.to_smulCommClass	—	Set.ext IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.right Algebra.to_smulCommClass SetLike.mem_coe StarAlgebra.adjoin_nonUnitalStarSubalgebra StarSubalgebra.mem_toSubalgebra Subalgebra.mem_toSubmodule StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span Submodule.mem_sup NonUnitalSubalgebra.smul_mem'
adjoin_id_eq_span_one_union 📖	mathematical	—	SetLike.coe StarSubalgebra ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar algebra Algebra.id instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing StarSubalgebra.setLike StarAlgebra.adjoin Set.instSingletonSet restrict id Submodule instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule.setLike Submodule.span Set.instUnion instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NonUnitalStarSubalgebra instNonUnitalSemiringOfIsTopologicalSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin IsScalarTower.right Algebra.to_smulCommClass	—	Set.ext IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.right Algebra.to_smulCommClass SetLike.mem_coe StarAlgebra.adjoin_nonUnitalStarSubalgebra StarSubalgebra.mem_toSubalgebra Subalgebra.mem_toSubmodule StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span Submodule.span_union NonUnitalStarAlgebra.span_eq_toSubmodule
algHom_ext_map_X 📖	—	Continuous ContinuousMap Set.Elem Real instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace compactOpen DFunLike.coe AlgHom Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id AlgHom.funLike Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.toContinuousMapOnAlgHom Polynomial.X	—	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal AlgHom.algHomClass instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact polynomialFunctions.topologicalClosure Subalgebra.topologicalClosure_minimal polynomialFunctions.le_equalizer isClosed_eq AlgHom.ext
attachBound_apply_coe 📖	mathematical	—	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instNeg Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe Set.Elem instTopologicalSpaceSubtype instFunLike attachBound	—	—
comp_attachBound_mem_closure 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing comp Set.Elem Set.Icc Real.instPreorder Real.instNeg Norm.norm NormedRing.toNorm Subalgebra.normedRing Real.commRing instNormedRing NormedCommRing.toNormedRing instTopologicalSpaceSubtype Set Set.instMembership attachBound	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal continuousMap_mem_polynomialFunctions_closure mem_closure_iff_frequently Filter.Tendsto.frequently_map ContinuousAt.tendsto continuousAt polynomial_comp_attachBound_mem
continuousMap_mem_subalgebra_closure_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Real Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal	ContinuousMap Subalgebra instSemiringOfIsTopologicalSemiring algebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NonUnitalSeminormedRing.toIsTopologicalRing subalgebra_topologicalClosure_eq_top_of_separatesPoints
elemental_id_eq_top 📖	mathematical	—	StarAlgebra.elemental ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing compactOpen instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NormedStarGroup.to_continuousStar instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing starAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing algebra Algebra.id instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing restrict id Top.top StarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice StarSubalgebra.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact NormedStarGroup.to_continuousStar SeminormedAddCommGroup.toIsTopologicalAddGroup instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing StarAlgebra.elemental.eq_1 polynomialFunctions.starClosure_topologicalClosure polynomialFunctions.starClosure_eq_adjoin_X Polynomial.toContinuousMap_X_eq_id
exists_mem_subalgebra_near_continuousMap_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Real Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal Real.instLT Real.instZero	Norm.norm ContinuousMap instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing instSubOfContinuousSub Real.instSub IsTopologicalAddGroup.to_continuousSub Real.instAddGroup instIsTopologicalAddGroupReal Subalgebra instSemiringOfIsTopologicalSemiring algebra SetLike.instMembership Subalgebra.instSetLike	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal mem_closure_iff_frequently continuousMap_mem_subalgebra_closure_of_separatesPoints IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.HasBasis.frequently_iff Metric.nhds_basis_ball dist_eq_norm Metric.mem_ball
exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Real Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal IsCompact Real.instLT Real.instZero	ContinuousMap Subalgebra instSemiringOfIsTopologicalSemiring algebra SetLike.instMembership Subalgebra.instSetLike Norm.norm Real.norm Real.instSub DFunLike.coe instFunLike	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal continuous_subtype_val StarAlgHom.instAlgHomClass Subtype.coe_ne_coe Subalgebra.mem_map exists_mem_subalgebra_near_continuous_of_separatesPoints isCompact_iff_compactSpace ContinuousOn.restrict Continuous.continuousOn continuous
exists_mem_subalgebra_near_continuous_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Real Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal Continuous Real.instLT Real.instZero	Norm.norm Real.norm Real.instSub DFunLike.coe ContinuousMap instFunLike Subalgebra instSemiringOfIsTopologicalSemiring algebra SetLike.instMembership Subalgebra.instSetLike	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal exists_mem_subalgebra_near_continuousMap_of_separatesPoints norm_lt_iff
induction_on 📖	—	const Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField restrict id Star.star ContinuousMap instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing StarRing.toStarAddMonoid RCLike.toStarRing RCLike.instContinuousStar instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul Distrib.toMul IsTopologicalSemiring.toContinuousMul	—	—	RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul instStarModule StarMul.toStarModule Algebra.adjoin_induction star_eq_iff_star_eq Polynomial.toContinuousMapOn_X_eq_restrict_id polynomialFunctions.starClosure_eq_adjoin_X
induction_on_of_compact 📖	—	const Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField restrict id Star.star ContinuousMap instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing StarRing.toStarAddMonoid RCLike.toStarRing RCLike.instContinuousStar instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul Distrib.toMul IsTopologicalSemiring.toContinuousMul	—	—	RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul induction_on instStarModule StarMul.toStarModule instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact NormedStarGroup.to_continuousStar SeminormedAddCommGroup.toIsTopologicalAddGroup instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing StarSubalgebra.mem_top polynomialFunctions.starClosure_topologicalClosure Filter.Frequently.mp mem_closure_iff_frequently StarSubalgebra.topologicalClosure_coe SetLike.mem_coe Filter.Eventually.of_forall
inf_mem_closed_subalgebra 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike inf Real.instSemilatticeInf TopologicalLattice.toContinuousInf Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal TopologicalLattice.toContinuousInf HasSolidNorm.toTopologicalLattice instHasSolidNormReal Real.instIsOrderedAddMonoid NonUnitalSeminormedRing.toIsTopologicalRing SetLike.ext' Subalgebra.topologicalClosure_coe closure_eq_iff_isClosed inf_mem_subalgebra_closure
inf_mem_subalgebra_closure 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing inf Real.instSemilatticeInf TopologicalLattice.toContinuousInf Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NonUnitalSeminormedRing.toIsTopologicalRing TopologicalLattice.toContinuousInf HasSolidNorm.toTopologicalLattice instHasSolidNormReal Real.instIsOrderedAddMonoid instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat inf_eq_half_smul_add_sub_abs_sub' ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Subalgebra.smul_mem Subalgebra.sub_mem Subalgebra.add_mem Subalgebra.le_topologicalClosure abs_mem_subalgebra_closure SubringClass.addSubgroupClass Subalgebra.instSubringClass
ker_evalStarAlgHom_eq_closure_adjoin_id 📖	mathematical	Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	SetLike.coe Ideal ContinuousMap instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Set.Elem Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker StarAlgHom algebra Algebra.id instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid RCLike.toStarRing RCLike.instContinuousStar StarAlgHom.instFunLike AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass evalStarAlgHom closure compactOpen NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring instNonUnitalSemiringOfIsTopologicalSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instStarRingOfContinuousStar NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.to_smulCommClass instStarModule StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Set.instSingletonSet restrict id	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.right Algebra.to_smulCommClass instStarModule StarMul.toStarModule ker_evalStarAlgHom_inter_adjoin_id AlgHom.closure_ker_inter T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup instIsTopologicalAddGroup instContinuousSMul ContinuousMul.to_continuousSMul AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass StarSubalgebra.subsemiringClass SubringClass.addSubgroupClass StarSubalgebra.subringClass StarSubalgebra.smulMemClass ContinuousEvalConst.continuous_eval_const instContinuousEvalConst Polynomial.toContinuousMapOn_X_eq_restrict_id Polynomial.toContinuousMapOnAlgHom_apply polynomialFunctions.starClosure_eq_adjoin_X instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact NormedStarGroup.to_continuousStar instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing polynomialFunctions.starClosure_topologicalClosure Set.univ_inter
ker_evalStarAlgHom_inter_adjoin_id 📖	mathematical	Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	ContinuousMap Set.Elem instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set.instInter SetLike.coe StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar algebra Algebra.id instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing StarSubalgebra.setLike StarAlgebra.adjoin Set.instSingletonSet restrict id Ideal Submodule.setLike Semiring.toModule RingHom.ker StarAlgHom instStar StarAlgHom.instFunLike AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass evalStarAlgHom NonUnitalStarSubalgebra instNonUnitalSemiringOfIsTopologicalSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin IsScalarTower.right Algebra.to_smulCommClass	—	Set.ext IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.right Algebra.to_smulCommClass SetLike.mem_coe IsTopologicalSemiring.toContinuousAdd adjoin_id_eq_span_one_add nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom mul_one smul_eq_mul one_apply smul_apply add_zero add_apply zero_smul zero_add NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin
nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom 📖	mathematical	Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	ContinuousMap Set.Elem instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set.instHasSubset SetLike.coe NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalSemiring.toNonUnitalNonAssocSemiring instNonUnitalSemiringOfIsTopologicalSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing module CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instStarRingOfContinuousStar RCLike.toStarRing RCLike.instContinuousStar NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin IsScalarTower.right instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebra Algebra.id Algebra.to_smulCommClass instStarModule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Set.instSingletonSet restrict id Ideal Submodule.setLike Semiring.toModule RingHom.ker StarAlgHom instStar StarAlgHom.instFunLike AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass evalStarAlgHom	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar IsScalarTower.right Algebra.to_smulCommClass instStarModule StarMul.toStarModule NonUnitalStarAlgebra.adjoin_induction AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass Set.mem_singleton_iff AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Ideal.mul_mem_left SetLike.mem_coe RingHom.mem_ker map_smul SemilinearMapClass.toMulActionSemiHomClass IsTopologicalSemiring.toContinuousAdd NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass smul_zero StarHomClass.map_star StarAlgHom.instStarHomClass star_zero
polynomial_comp_attachBound 📖	mathematical	—	comp Set.Elem Real Set.Icc Real.instPreorder Real.instNeg Norm.norm ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike NormedRing.toNorm Subalgebra.normedRing Real.commRing instNormedRing NormedCommRing.toNormedRing instTopologicalSpaceSubtype Set Set.instMembership Polynomial.toContinuousMapOn attachBound DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Subalgebra.toSemiring Polynomial.algebraOfAlgebra Subalgebra.algebra AlgHom.funLike Polynomial.aeval	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ext Polynomial.aeval_subalgebra_coe Polynomial.aeval_continuousMap_apply
polynomial_comp_attachBound_mem 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike comp Set.Elem Set.Icc Real.instPreorder Real.instNeg Norm.norm NormedRing.toNorm Subalgebra.normedRing Real.commRing instNormedRing NormedCommRing.toNormedRing instTopologicalSpaceSubtype Set Set.instMembership Polynomial.toContinuousMapOn attachBound	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal polynomial_comp_attachBound SetLike.coe_mem
starAlgHom_ext_map_X 📖	—	Continuous ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField compactOpen DFunLike.coe StarAlgHom Semifield.toCommSemiring Field.toSemifield NormedField.toField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing algebra Algebra.id instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid RCLike.toStarRing RCLike.instContinuousStar Ring.toSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra AlgHom.funLike Polynomial.toContinuousMapOnAlgHom Polynomial.X	—	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule StarAlgHom.instAlgHomClass StarAlgHom.instStarHomClass instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact NormedStarGroup.to_continuousStar SeminormedAddCommGroup.toIsTopologicalAddGroup instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing polynomialFunctions.starClosure_topologicalClosure StarSubalgebra.topologicalClosure_minimal polynomialFunctions.starClosure_le_equalizer isClosed_eq StarAlgHom.ext StarSubalgebra.mem_top
starSubalgebra_topologicalClosure_eq_top_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing StarSubalgebra.toSubalgebra ContinuousMap RCLike.toStarRing instSemiringOfIsTopologicalSemiring instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar algebra instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing	StarSubalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedStarGroup.to_continuousStar instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup starAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing Top.top StarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice StarSubalgebra.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instStarModule StarMul.toStarModule NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar SeminormedAddCommGroup.toIsTopologicalAddGroup instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing StarSubalgebra.eq_top_iff IsTopologicalSemiring.toContinuousAdd instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomSurjective.ids instContinuousConstSMul instIsScalarTower IsScalarTower.right RCLike.continuous_ofReal subalgebra_topologicalClosure_eq_top_of_separatesPoints Subalgebra.SeparatesPoints.rclike_to_real Submodule.map_top ContinuousSMul.continuousConstSMul instContinuousSMul ContinuousMul.to_continuousSMul IsBoundedSMul.continuousSMul Submodule.topologicalClosure_map Submodule.map_comap_le LE.le.trans Submodule.topologicalClosure_mono ContinuousLinearMap.continuous Subalgebra.add_mem StarSubalgebra.smul_mem ext mul_comm RCLike.re_add_im StarSubalgebra.mem_toSubalgebra
subalgebra_topologicalClosure_eq_top_of_separatesPoints 📖	mathematical	Subalgebra.SeparatesPoints Real Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal	Subalgebra.topologicalClosure ContinuousMap instSemiringOfIsTopologicalSemiring compactOpen algebra instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal SetLike.ext' NonUnitalSeminormedRing.toIsTopologicalRing Subalgebra.le_topologicalClosure Subalgebra.one_mem IsClosed.closure_eq sublattice_closure_eq_top inf_mem_closed_subalgebra Subalgebra.isClosed_topologicalClosure sup_mem_closed_subalgebra Subalgebra.SeparatesPoints.strongly Subalgebra.separatesPoints_monotone
sublattice_closure_eq_top 📖	mathematical	Set.Nonempty ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set Set.instMembership inf Real.instSemilatticeInf TopologicalLattice.toContinuousInf Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid sup Real.instSemilatticeSup TopologicalLattice.toContinuousSup Set.SeparatesPointsStrongly	closure compactOpen Top.top BooleanAlgebra.toTop Set.instBooleanAlgebra	—	TopologicalLattice.toContinuousInf HasSolidNorm.toTopologicalLattice instHasSolidNormReal Real.instIsOrderedAddMonoid TopologicalLattice.toContinuousSup eq_top_iff Filter.Frequently.mem_closure Filter.HasBasis.frequently_iff Metric.nhds_basis_ball IsOpen.mem_nhds isOpen_lt HasSolidNorm.orderClosedTopology Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal ContinuousMapClass.map_continuous instContinuousMapClass continuous_const Set.mem_setOf_eq sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono CompactSpace.elim_nhds_subcover Set.nonempty_of_union_eq_top_of_nonempty Finset.sup'_mem Set.exists_set_mem_of_union_eq_top coe_sup' Finset.sup'_apply Finset.sup'_congr Finset.sup'_const Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal lt_add_of_pos_right Finset.inf'_mem dist_lt_iff Real.ball_eq_Ioo inf'_apply
sup_mem_closed_subalgebra 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike sup Real.instSemilatticeSup TopologicalLattice.toContinuousSup Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal TopologicalLattice.toContinuousSup HasSolidNorm.toTopologicalLattice instHasSolidNormReal Real.instIsOrderedAddMonoid NonUnitalSeminormedRing.toIsTopologicalRing SetLike.ext' closure_eq_iff_isClosed sup_mem_subalgebra_closure
sup_mem_subalgebra_closure 📖	mathematical	—	ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure compactOpen instNonUnitalNonAssocRingOfIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing instNonUnitalSeminormedRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing sup Real.instSemilatticeSup TopologicalLattice.toContinuousSup Real.lattice HasSolidNorm.toTopologicalLattice Real.normedAddCommGroup instHasSolidNormReal Real.instIsOrderedAddMonoid	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NonUnitalSeminormedRing.toIsTopologicalRing TopologicalLattice.toContinuousSup HasSolidNorm.toTopologicalLattice instHasSolidNormReal Real.instIsOrderedAddMonoid instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat sup_eq_half_smul_add_add_abs_sub' ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Subalgebra.smul_mem Subalgebra.add_mem Subalgebra.le_topologicalClosure abs_mem_subalgebra_closure SubringClass.addSubgroupClass Subalgebra.instSubringClass

ContinuousMap.AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_ker_inter 📖	mathematical	Continuous DFunLike.coe	closure Set Set.instInter SetLike.coe Ideal Ring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker CommSemiring.toSemiring CommRing.toCommSemiring AlgHomClass.toRingHomClass Algebra.id	—	subset_antisymm AlgHomClass.toRingHomClass Set.instAntisymmSubset IsClosed.closure_eq IsClosed.preimage isClosed_singleton closure_inter_subset_inter_closure sub_zero zero_smul Filter.tendsto_inf_left Continuous.tendsto Continuous.sub continuous_id' Continuous.smul continuous_const mem_closure_of_tendsto ClusterPt.eq_1 mem_closure_iff_clusterPt Filter.eventually_inf_principal Filter.univ_mem' sub_mem SMulMemClass.smul_mem OneMemClass.one_mem map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_one sub_self

ContinuousMapZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_id_dense 📖	mathematical	—	Dense ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instTopologicalSpace SetLike.coe NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing CommSemiring.toSemiring NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instStarRing RCLike.toStarRing RCLike.instContinuousStar NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.adjoin instIsScalarTower' IsScalarTower.right Algebra.id instSMulCommClass' Algebra.to_smulCommClass instStarModule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Set.instSingletonSet id	—	Fact.out IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar instIsScalarTower' IsScalarTower.right instSMulCommClass' Algebra.to_smulCommClass instStarModule StarMul.toStarModule dense_iff_closure_eq instContinuousMapClass Function.Injective.preimage_image Topology.IsEmbedding.injective Topology.IsClosedEmbedding.toIsEmbedding isClosedEmbedding_toContinuousMap T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Topology.IsClosedEmbedding.closure_image_eq IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul coe_toContinuousMapHom NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarSubalgebra.coe_map ContinuousMap.instStarModule NonUnitalStarAlgHom.map_adjoin_singleton toContinuousMapHom_apply toContinuousMap_id AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id Set.eq_univ_of_forall map_zero instZeroHomClass
elemental_eq_top 📖	mathematical	—	NonUnitalStarAlgebra.elemental ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing NonUnitalCommSemiring.toNonUnitalSemiring instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instStarRing RCLike.instContinuousStar instModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing CommSemiring.toSemiring NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instIsScalarTower' IsScalarTower.right Algebra.id instSMulCommClass' Algebra.to_smulCommClass instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing instTopologicalSpace instNonUnitalCommRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing instNonUnitalNormedCommRing instUniformSpace IsBoundedSMul.toUniformContinuousConstSMul NonUnitalSeminormedRing.toPseudoMetricSpace instZero NormedSpace.toIsBoundedSMul instNormedSpaceOfNormedAlgebra NormedAlgebra.id NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup instCStarRing RCLike.instCStarRing id Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar instIsScalarTower' IsScalarTower.right instSMulCommClass' Algebra.to_smulCommClass instStarModule StarMul.toStarModule NonUnitalSeminormedRing.toIsTopologicalRing IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup instCStarRing RCLike.instCStarRing SetLike.ext'_iff Dense.closure_eq adjoin_id_dense
induction_on 📖	—	ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instZero id Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing StarRing.toStarAddMonoid instStarRing Semifield.toCommSemiring Field.toSemifield IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar instAdd AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalSemiring.toContinuousAdd instMul IsTopologicalSemiring.toContinuousMul instSMul DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalRing.toIsTopologicalSemiring RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup instIsScalarTower' IsScalarTower.right instSMulCommClass' Algebra.to_smulCommClass instStarModule StarMul.toStarModule NonUnitalAlgebra.adjoin_induction star_eq_iff_star_eq
induction_on_of_compact 📖	—	ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instZero id Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing StarRing.toStarAddMonoid instStarRing Semifield.toCommSemiring Field.toSemifield IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar instAdd AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalSemiring.toContinuousAdd instMul IsTopologicalSemiring.toContinuousMul instSMul DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalRing.toIsTopologicalSemiring RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup induction_on instIsScalarTower' IsScalarTower.right instSMulCommClass' Algebra.to_smulCommClass instStarModule StarMul.toStarModule Set.mem_univ Dense.closure_eq adjoin_id_dense Filter.Frequently.mp mem_closure_iff_frequently Filter.Eventually.of_forall
mul_nonUnitalStarAlgHom_apply_eq_zero 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instModule NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instStarRing Semifield.toCommSemiring RCLike.toStarRing RCLike.instContinuousStar NonUnitalStarAlgHom.instFunLike id Star.star Continuous instTopologicalSpace	—	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar induction_on_of_compact map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass MulZeroClass.mul_zero map_add AddMonoidHomClass.toAddHomClass mul_add Distrib.leftDistribClass zero_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass MulZeroClass.zero_mul map_smul DistribMulActionSemiHomClass.toMulActionSemiHomClass mul_smul_comm smul_zero Filter.Frequently.mem_of_closed isClosed_eq Continuous.comp' Continuous.fun_mul Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const continuous_zero
nonUnitalStarAlgHom_apply_mul_eq_zero 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instModule NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instStarRing Semifield.toCommSemiring RCLike.toStarRing RCLike.instContinuousStar NonUnitalStarAlgHom.instFunLike id Star.star Continuous instTopologicalSpace	—	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar induction_on_of_compact map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass MulZeroClass.zero_mul map_add AddMonoidHomClass.toAddHomClass add_mul Distrib.rightDistribClass zero_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass mul_assoc MulZeroClass.mul_zero map_smul DistribMulActionSemiHomClass.toMulActionSemiHomClass smul_mul_assoc smul_zero Filter.Frequently.mem_of_closed isClosed_eq Continuous.comp' Continuous.fun_mul Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const continuous_zero

Subalgebra.SeparatesPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rclike_to_real 📖	mathematical	Subalgebra.SeparatesPoints Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing StarSubalgebra.toSubalgebra ContinuousMap RCLike.toStarRing ContinuousMap.instSemiringOfIsTopologicalSemiring ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar ContinuousMap.algebra ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing	Real Real.instCommSemiring Real.pseudoMetricSpace Real.semiring Real.normedCommRing instIsTopologicalRingReal Subalgebra.comap NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra AlgHom.compLeftContinuous RCLike.ofRealAm RCLike.continuous_ofReal Subalgebra.restrictScalars ContinuousMap.instIsScalarTower IsScalarTower.right SeminormedRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule instIsTopologicalRingReal RCLike.continuous_ofReal ContinuousMap.instIsScalarTower IsScalarTower.right IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Subalgebra.sub_mem ContinuousMap.ext mul_one StarSubalgebra.smul_mem Subalgebra.one_mem Continuous.comp' Continuous.pow IsTopologicalSemiring.toContinuousMul continuous_id' Continuous.norm ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass SetLike.mem_coe Subalgebra.mem_comap map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Subalgebra.mul_mem StarMemClass.star_mem StarSubalgebra.starMemClass sub_self norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sub_ne_zero

polynomialFunctions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
starClosure_topologicalClosure 📖	mathematical	—	StarSubalgebra.topologicalClosure ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing ContinuousMap.compactOpen ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain StarRing.toStarMul Ring.toSemiring CommRing.toRing ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NormedStarGroup.to_continuousStar ContinuousMap.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousMap.starAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring ContinuousMap.instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing Subalgebra.starClosure polynomialFunctions Top.top StarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice StarSubalgebra.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule Subalgebra.separatesPoints_monotone le_sup_left polynomialFunctions_separatesPoints
topologicalClosure 📖	mathematical	—	Subalgebra.topologicalClosure Real Real.instCommSemiring ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.compactOpen ContinuousMap.algebra Algebra.id ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring polynomialFunctions Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal polynomialFunctions_separatesPoints

---

← Back to Index