Range

📁 Source: Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean

Statistics

Metric	Count
Definitions	0
Theorems cfcHom_apply_mem_elemental, cfc_apply_mem_elemental, cfcₙHom_apply_mem_elemental, cfcₙ_apply_mem_elemental, range_cfc, range_cfcHom, range_cfc_nnreal, range_cfc_nnreal_eq_image_cfc_real, range_cfcₙ, range_cfcₙHom, range_cfcₙ_nnreal, range_cfcₙ_nnreal_eq_image_cfcₙ_real	12
Total	12

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcHom_apply_mem_elemental 📖	mathematical	—	StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing Ring.toSemiring SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring StarAlgHom.instFunLike cfcHom	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar range_cfcHom
cfc_apply_mem_elemental 📖	mathematical	—	StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing Ring.toSemiring SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc NormedField.toMetricSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfc_cases ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass StarSubalgebra.subsemiringClass cfcHom_apply_mem_elemental ContinuousOn.restrict
cfcₙHom_apply_mem_elemental 📖	mathematical	—	NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental RCLike.toStarRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule SMulCommClass.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul Semiring.toNonUnitalSemiring ContinuousMapZero.instStarRing RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass range_cfcₙHom
cfcₙ_apply_mem_elemental 📖	mathematical	—	NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental RCLike.toStarRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing NormedField.toMetricSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_cases ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass ContinuousOn.restrict cfcₙHom_apply_mem_elemental
range_cfc 📖	mathematical	—	Set.range cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SetLike.coe StarSubalgebra Ring.toSemiring StarSubalgebra.setLike StarAlgebra.elemental NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar range_cfc_eq_range_cfcHom range_cfcHom
range_cfcHom 📖	mathematical	—	StarAlgHom.range ContinuousMap Set.Elem spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace RCLike.toStarRing ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring RCLike.instContinuousStar Ring.toSemiring cfcHom StarAlgebra.elemental NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule StarAlgHom.range_eq_map_top ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact ContinuousFunctionalCalculus.compactSpace_spectrum NormedStarGroup.to_continuousStar SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMap.instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing ContinuousMap.elemental_id_eq_top StarAlgebra.elemental.eq_1 StarSubalgebra.topologicalClosure_map Topology.IsClosedEmbedding.isClosedMap cfcHom_isClosedEmbedding cfcHom_continuous StarAlgHom.map_adjoin Set.image_singleton cfcHom_id
range_cfc_nnreal 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.range cfc NNReal instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus setOf StarSubalgebra Real Real.instCommSemiring instStarRingReal SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsTopologicalRing.toIsTopologicalSemiring	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus range_cfc_nnreal_eq_image_cfc_real Set.setOf_and SetLike.setOf_mem_eq IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar range_cfc LE.le.isSelfAdjoint Set.inter_comm Set.image_preimage_eq_inter_range Set.Subset.antisymm Set.image_mono cfc_nonneg Real.instStarOrderedRing em cfc_nonneg_iff cfc_zero cfc_apply_of_not_continuousOn cfc_apply_of_not_predicate
range_cfc_nnreal_eq_image_cfc_real 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.range cfc NNReal instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus Set.image Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal setOf	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Set.ext NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus cfc_nnreal_eq_real NNReal.coe_nonneg cfc_real_eq_nnreal
range_cfcₙ 📖	mathematical	—	Set.range cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental NonUnitalRing.toNonUnitalNonAssocRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass range_cfcₙ_eq_range_cfcₙHom UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup range_cfcₙHom
range_cfcₙHom 📖	mathematical	—	NonUnitalStarAlgHom.range NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule SMulCommClass.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid ContinuousMapZero.instStarRing RCLike.toStarRing RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass cfcₙHom NonUnitalStarAlgebra.elemental NonUnitalRing.toNonUnitalSemiring	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass ContinuousMapZero.instIsScalarTower' IsScalarTower.right ContinuousMapZero.instSMulCommClass' ContinuousMapZero.instStarModule StarMul.toStarModule NonUnitalStarAlgebra.map_top instFactMemSetQuasispectrumOfNat NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup ContinuousMapZero.instCStarRing RCLike.instCStarRing ContinuousMapZero.elemental_eq_top NonUnitalStarAlgebra.elemental.eq_1 NonUnitalStarSubalgebra.topologicalClosure_map Topology.IsClosedEmbedding.isClosedMap cfcₙHom_isClosedEmbedding cfcₙHom_continuous NonUnitalStarAlgHom.map_adjoin Set.image_singleton cfcₙHom_id
range_cfcₙ_nnreal 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Set.range cfcₙ NNReal instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus setOf NonUnitalStarSubalgebra Real.instCommSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental instStarRingReal IsTopologicalRing.toIsTopologicalSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus range_cfcₙ_nnreal_eq_image_cfcₙ_real Set.setOf_and SetLike.setOf_mem_eq IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar range_cfcₙ LE.le.isSelfAdjoint Set.inter_comm Set.image_preimage_eq_inter_range Set.Subset.antisymm Set.image_mono cfcₙ_nonneg Real.instStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass em cfcₙ_nonneg_iff cfcₙ_zero cfcₙ_apply_of_not_continuousOn cfcₙ_apply_of_not_map_zero cfcₙ_apply_of_not_predicate
range_cfcₙ_nnreal_eq_image_cfcₙ_real 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Set.range cfcₙ NNReal instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus Set.image IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal setOf	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Set.ext NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus cfcₙ_nnreal_eq_real NNReal.coe_nonneg cfcₙ_real_eq_nnreal

---

← Back to Index