StarSubalgebra

📁 Source: Mathlib/Topology/Algebra/StarSubalgebra.lean

Statistics

Metric	Count
Definitions elemental, instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal, instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal, StarSubalgebra, commRingTopologicalClosure, commSemiringTopologicalClosure, topologicalClosure	7
Theorems ext_topologicalClosure, ext_topologicalClosure, induction_on, instCompleteSpaceSubtypeMemStarSubalgebra, isClosed, isClosedEmbedding_coe, le_centralizer_centralizer, le_iff_mem, le_of_mem, self_mem, starAlgHomClass_ext, star_self_mem, instCompleteSpaceSubtypeMemTopologicalClosure, instIsSemitopologicalSemiringSubtypeMem, instIsTopologicalSemiringSubtypeMem, isClosedEmbedding_inclusion, isClosed_topologicalClosure, isEmbedding_inclusion, le_topologicalClosure, map_topologicalClosure_le, topologicalClosure_adjoin_le_centralizer_centralizer, topologicalClosure_coe, topologicalClosure_map, topologicalClosure_map_le, topologicalClosure_minimal, topologicalClosure_mono, topologicalClosure_toSubalgebra_comm, topologicalClosure_star_comm	28
Total	35

StarAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_topologicalClosure 📖	—	Continuous StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarSubalgebra.topologicalClosure instTopologicalSpaceSubtype DFunLike.coe StarAlgHom SubsemiringClass.toSemiring StarSubalgebra.subsemiringClass StarSubalgebra.algebra StarMemClass.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarSubalgebra.starMemClass instFunLike comp StarSubalgebra.inclusion StarSubalgebra.le_topologicalClosure	—	—	StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass StarSubalgebra.le_topologicalClosure DFunLike.ext'_iff Set.instReflSubset Continuous.ext_on DFunLike.congr_fun

StarAlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_topologicalClosure 📖	—	Continuous StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarSubalgebra.topologicalClosure instTopologicalSpaceSubtype DFunLike.coe StarAlgHom SubsemiringClass.toSemiring StarSubalgebra.subsemiringClass StarSubalgebra.algebra StarMemClass.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarSubalgebra.starMemClass StarAlgHom.instFunLike StarSubalgebra.inclusion StarSubalgebra.le_topologicalClosure	—	—	StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass StarSubalgebra.le_topologicalClosure StarAlgHom.ext_topologicalClosure StarAlgHom.ext DFunLike.ext'_iff StarAlgHom.coe_coe

StarAlgebra

Definitions

Name	Category	Theorems
elemental 📖	CompOp	24 math math: cfc_mem_elemental, elemental.characterSpaceToSpectrum_coe, cfcHom_mem_elemental, elemental.isClosed, elemental.le_of_mem, range_cfc_subset, elemental.le_iff_mem, elemental.bijective_characterSpaceToSpectrum, elemental.le_centralizer_centralizer, elemental.instCompleteSpaceSubtypeMemStarSubalgebra, elemental.star_self_mem, range_cfc_nnreal, elemental.self_mem, cfc_apply_mem_elemental, elemental.isClosedEmbedding_coe, range_cfcHom_le, ContinuousMap.elemental_id_eq_top, range_cfcHom, elemental.continuous_characterSpaceToSpectrum, cfcHom_eq_of_isStarNormal, range_cfc, range_cfc_nnreal_subset, continuousFunctionalCalculus_map_id, cfcHom_apply_mem_elemental

StarAlgebra.elemental

Definitions

Name	Category	Theorems
instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal 📖	CompOp	—
instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on 📖	—	StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental self_mem Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid star_self_mem DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.addSubmonoidWithOneClass StarSubalgebra.subsemiringClass StarSubalgebra.smulMemClass Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid SubsemiringClass.toAddSubmonoidClass Distrib.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SubsemiringClass.toSubmonoidClass closure_minimal SetLike.coe isClosed	—	—	self_mem star_self_mem algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass StarSubalgebra.subsemiringClass StarSubalgebra.smulMemClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass closure_minimal isClosed subset_closure Algebra.adjoin_induction star_star StarAlgebra.adjoin_toSubalgebra StarSubalgebra.mem_toSubalgebra SetLike.mem_coe
instCompleteSpaceSubtypeMemStarSubalgebra 📖	mathematical	—	CompleteSpace StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental UniformSpace.toTopologicalSpace instUniformSpaceSubtype	—	IsClosed.completeSpace_coe isClosed_closure
isClosed 📖	mathematical	—	IsClosed SetLike.coe StarSubalgebra StarSubalgebra.setLike StarAlgebra.elemental	—	isClosed_closure
isClosedEmbedding_coe 📖	mathematical	—	Topology.IsClosedEmbedding StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental instTopologicalSpaceSubtype	—	Subtype.coe_injective Subtype.range_coe_subtype isClosed
le_centralizer_centralizer 📖	mathematical	—	StarSubalgebra Preorder.toLE PartialOrder.toPreorder StarSubalgebra.instPartialOrder StarAlgebra.elemental StarSubalgebra.centralizer SetLike.coe StarSubalgebra.setLike Set Set.instSingletonSet	—	StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer
le_iff_mem 📖	mathematical	—	StarSubalgebra Preorder.toLE PartialOrder.toPreorder StarSubalgebra.instPartialOrder StarAlgebra.elemental SetLike.instMembership StarSubalgebra.setLike	—	self_mem le_of_mem
le_of_mem 📖	mathematical	StarSubalgebra SetLike.instMembership StarSubalgebra.setLike	StarSubalgebra Preorder.toLE PartialOrder.toPreorder StarSubalgebra.instPartialOrder StarAlgebra.elemental	—	StarSubalgebra.topologicalClosure_minimal StarAlgebra.adjoin_le Set.singleton_subset_iff
self_mem 📖	mathematical	—	StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental	—	StarSubalgebra.le_topologicalClosure StarAlgebra.self_mem_adjoin_singleton
starAlgHomClass_ext 📖	—	Continuous StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental instTopologicalSpaceSubtype DFunLike.coe self_mem	—	—	StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass self_mem StarAlgHomClass.ext_topologicalClosure StarAlgebra.adjoin_induction_subtype StarSubalgebra.le_topologicalClosure StarAlgebra.subset_adjoin Set.mem_singleton_iff AlgHomClass.commutes StarAlgHom.instAlgHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass StarHomClass.map_star StarAlgHom.instStarHomClass
star_self_mem 📖	mathematical	—	StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid	—	StarMemClass.star_mem StarSubalgebra.starMemClass self_mem

StarSubalgebra

Definitions

Name	Category	Theorems
commRingTopologicalClosure 📖	CompOp	—
commSemiringTopologicalClosure 📖	CompOp	—
topologicalClosure 📖	CompOp	15 math math: UnitAddTorus.mFourierSubalgebra_closure_eq_top, polynomialFunctions.starClosure_topologicalClosure, topologicalClosure_map_le, topologicalClosure_coe, isClosed_topologicalClosure, topologicalClosure_map, topologicalClosure_mono, topologicalClosure_minimal, topologicalClosure_adjoin_le_centralizer_centralizer, fourierSubalgebra_closure_eq_top, map_topologicalClosure_le, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, topologicalClosure_toSubalgebra_comm, le_topologicalClosure, instCompleteSpaceSubtypeMemTopologicalClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompleteSpaceSubtypeMemTopologicalClosure 📖	mathematical	—	CompleteSpace StarSubalgebra SetLike.instMembership setLike topologicalClosure UniformSpace.toTopologicalSpace instUniformSpaceSubtype	—	IsClosed.completeSpace_coe isClosed_closure
instIsSemitopologicalSemiringSubtypeMem 📖	mathematical	—	IsSemitopologicalSemiring StarSubalgebra SetLike.instMembership setLike instTopologicalSpaceSubtype NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SubsemiringClass.toSemiring subsemiringClass	—	Subsemiring.semitopologicalSemiring
instIsTopologicalSemiringSubtypeMem 📖	mathematical	—	IsTopologicalSemiring StarSubalgebra SetLike.instMembership setLike instTopologicalSpaceSubtype NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SubsemiringClass.toSemiring subsemiringClass	—	Subsemiring.topologicalSemiring
isClosedEmbedding_inclusion 📖	mathematical	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	Topology.IsClosedEmbedding StarSubalgebra SetLike.instMembership setLike instTopologicalSpaceSubtype DFunLike.coe StarAlgHom SubsemiringClass.toSemiring subsemiringClass algebra StarMemClass.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid starMemClass StarAlgHom.instFunLike inclusion	—	Topology.IsEmbedding.inclusion subsemiringClass starMemClass isClosed_induced_iff Set.image_id Set.range_subtype_map
isClosed_topologicalClosure 📖	mathematical	—	IsClosed SetLike.coe StarSubalgebra setLike topologicalClosure	—	isClosed_closure
isEmbedding_inclusion 📖	mathematical	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	Topology.IsEmbedding StarSubalgebra SetLike.instMembership setLike instTopologicalSpaceSubtype DFunLike.coe StarAlgHom SubsemiringClass.toSemiring subsemiringClass algebra StarMemClass.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid starMemClass StarAlgHom.instFunLike inclusion	—	subsemiringClass starMemClass induced_compose Subtype.map_injective
le_topologicalClosure 📖	mathematical	—	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder topologicalClosure	—	subset_closure
map_topologicalClosure_le 📖	mathematical	Continuous DFunLike.coe StarAlgHom InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarAlgHom.instFunLike	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder map topologicalClosure	—	image_closure_subset_closure_image
topologicalClosure_adjoin_le_centralizer_centralizer 📖	mathematical	—	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder topologicalClosure StarAlgebra.adjoin centralizer SetLike.coe setLike	—	topologicalClosure_minimal StarAlgebra.adjoin_le_centralizer_centralizer Set.isClosed_centralizer IsSemitopologicalSemiring.toSeparatelyContinuousMul
topologicalClosure_coe 📖	mathematical	—	SetLike.coe StarSubalgebra setLike topologicalClosure closure	—	—
topologicalClosure_map 📖	mathematical	IsClosedMap DFunLike.coe StarAlgHom InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarAlgHom.instFunLike Continuous	topologicalClosure map	—	SetLike.coe_injective IsClosedMap.closure_image_eq_of_continuous
topologicalClosure_map_le 📖	mathematical	IsClosedMap DFunLike.coe StarAlgHom InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarAlgHom.instFunLike	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder topologicalClosure map	—	IsClosedMap.closure_image_subset
topologicalClosure_minimal 📖	mathematical	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	StarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder topologicalClosure	—	closure_minimal
topologicalClosure_mono 📖	mathematical	—	Monotone StarSubalgebra PartialOrder.toPreorder instPartialOrder topologicalClosure	—	topologicalClosure_minimal LE.le.trans le_topologicalClosure isClosed_topologicalClosure
topologicalClosure_toSubalgebra_comm 📖	mathematical	—	toSubalgebra topologicalClosure Subalgebra.topologicalClosure	—	SetLike.coe_injective

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalClosure_star_comm 📖	mathematical	—	topologicalClosure Star.star Subalgebra InvolutiveStar.toStar involutiveStar	—	topologicalClosure_minimal star_mono subset_closure IsClosed.preimage ContinuousStar.continuous_star isClosed_closure le_antisymm topologicalClosure.congr_simp star_star

(root)

Definitions

Name	Category	Theorems
StarSubalgebra 📖	CompData	146 math math: StarSubalgebra.mem_toSubalgebra, StarSubalgebra.coe_sInf, StarAlgEquiv.ofInjective_symm_apply, StarAlgHom.mem_equalizer, Subalgebra.starClosure_le, StarSubalgebra.map_inf, StarSubalgebra.inclusion_apply, cfc_mem_elemental, StarSubalgebra.coe_map, StarSubalgebra.mem_sup_left, StarSubalgebra.range_le, StarSubalgebra.smulMemClass, StarAlgebra.elemental.characterSpaceToSpectrum_coe, StarSubalgebra.inf_toSubalgebra, StarSubalgebra.mem_toNonUnitalStarSubalgebra, StarSubalgebra.subringClass, StarAlgebra.adjoin_eq, StarAlgebra.isMulCommutative_adjoin, NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe, UnitAddTorus.mFourierSubalgebra_closure_eq_top, StarSubalgebra.subtype_comp_inclusion, cfcHom_mem_elemental, polynomialFunctions.starClosure_topologicalClosure, StarSubalgebra.toNonUnitalStarSubalgebra_injective, StarSubalgebra.ofClass_carrier, StarSubalgebra.bot_toSubalgebra, StarAlgEquiv.ofInjective_apply, StarAlgebra.self_mem_adjoin_singleton, StarSubalgebra.topologicalClosure_map_le, StarSubalgebra.comap_mono, StarSubalgebra.subsemiringClass, StarAlgebra.elemental.isClosed, StarSubalgebra.mem_bot, StarSubalgebra.mem_comap, polynomialFunctions.starClosure_le_equalizer, StarAlgebra.elemental.le_of_mem, range_cfc_subset, BoundedContinuousFunction.mem_charPoly, StarSubalgebra.mul_mem_sup, StarAlgebra.elemental.le_iff_mem, StarAlgHom.coe_codRestrict, StarSubalgebra.subtype_apply, StarSubalgebra.ext_iff, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, StarSubalgebra.isClosedEmbedding_inclusion, StarSubalgebra.instIsTopologicalSemiringSubtypeMem, Subalgebra.mem_starClosure, VonNeumannAlgebra.coe_mk, StarSubalgebra.eq_top_iff, VonNeumannAlgebra.mem_carrier, StarSubalgebra.topologicalClosure_coe, StarSubalgebra.spectrum_eq, StarSubalgebra.gc_map_comap, ContinuousMap.adjoin_id_eq_span_one_union, StarSubalgebra.coe_subtype, StarAlgebra.star_self_mem_adjoin_singleton, StarSubalgebra.coe_bot, StarSubalgebra.instIsSemitopologicalSemiringSubtypeMem, StarSubalgebra.comap_injective, StarAlgebra.star_subset_adjoin, Subalgebra.starClosure_le_iff, StarAlgHom.adjoin_le_equalizer, StarAlgebra.subset_adjoin, StarSubalgebra.isClosed_topologicalClosure, StarAlgebra.elemental.le_centralizer_centralizer, StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra, StarSubalgebra.toSubalgebra_injective, StarAlgebra.elemental.star_self_mem, StarSubalgebra.mem_iInf, range_cfc_eq_range_cfcHom, StarAlgebra.adjoin_le_centralizer_centralizer, StarSubalgebra.algebraMap_mem, StarSubalgebra.mem_carrier, StarSubalgebra.topologicalClosure_mono, StarSubalgebra.map_injective, StarSubalgebra.coe_mk, range_cfc_nnreal, StarSubalgebra.toSubalgebra_le_iff, StarSubalgebra.toSubalgebra_eq_top, StarSubalgebra.mem_top, StarSubalgebra.range_subset, StarAlgebra.elemental.self_mem, StarSubalgebra.coe_copy, cfc_apply_mem_elemental, StarAlgebra.gc, StarSubalgebra.map_sup, StarSubalgebra.starModule, StarSubalgebra.topologicalClosure_minimal, StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, StarSubalgebra.mem_spectrum_iff, StarSubalgebra.centralizer_le, StarAlgebra.isMulCommutative_adjoin_singleton, StarSubalgebra.coe_centralizer_centralizer, StarAlgebra.adjoin_le_iff, StarSubalgebra.to_cstarRing, StarAlgebra.elemental.isClosedEmbedding_coe, StarSubalgebra.coe_comap, StarSubalgebra.toSubalgebra_subtype, range_cfcHom_le, ContinuousMap.adjoin_id_eq_span_one_add, StarSubalgebra.mem_centralizer_iff, StarSubalgebra.smul_mem, StarSubalgebra.sInf_toSubalgebra, StarSubalgebra.coe_inf, Subalgebra.coe_starClosure, VonNeumannAlgebra.coe_toStarSubalgebra, StarSubalgebra.coe_isUnit, StarSubalgebra.coe_top, StarAlgHom.subtype_comp_codRestrict, fourierSubalgebra_closure_eq_top, StarSubalgebra.map_le_iff_le_comap, StarSubalgebra.coe_iInf, StarSubalgebra.mem_sInf, StarSubalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar, StarSubalgebra.coe_centralizer, StarSubalgebra.inclusion_injective, StarAlgebra.adjoin_le, StarAlgHom.range_eq_map_top, StarAlgebra.instIsMulCommutative_adjoin, StarSubalgebra.mem_sup_right, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, StarSubalgebra.map_topologicalClosure_le, StarAlgebra.adjoin_mono, ContinuousMap.elemental_id_eq_top, Unitization.starLift_range_le, StarSubalgebra.mem_inf, StarSubalgebra.coe_toSubalgebra, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, StarSubalgebra.mem_map, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, StarSubalgebra.map_iInf, cfcHom_eq_of_isStarNormal, StarAlgHom.injective_codRestrict, range_cfc, range_cfc_nnreal_subset, StarSubalgebra.starMemClass, StarSubalgebra.isEmbedding_inclusion, StarSubalgebra.iInf_toSubalgebra, StarSubalgebra.map_mono, StarSubalgebra.top_toSubalgebra, continuousFunctionalCalculus_map_id, StarSubalgebra.le_topologicalClosure, StarAlgebra.mem_adjoin_of_mem, cfcHom_apply_mem_elemental, StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure, BoundedContinuousFunction.char_mem_charPoly

---

← Back to Index