Range

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

Statistics

Metric	Count
Definitions	0
Theorems cfcHom_apply_mem_elemental, cfcHom_mem_elemental, cfc_apply_mem_elemental, cfc_mem, cfc_mem_elemental, cfcₙHom_apply_mem_elemental, cfcₙHom_mem_elemental, cfcₙ_apply_mem_elemental, cfcₙ_mem, cfcₙ_mem_elemental, range_cfc, range_cfcHom, range_cfcHom_le, range_cfc_nnreal, range_cfc_nnreal_eq_image_cfc_real, range_cfc_nnreal_subset, range_cfc_subset, range_cfcₙ, range_cfcₙHom, range_cfcₙHom_le, range_cfcₙ_nnreal, range_cfcₙ_nnreal_eq_image_cfcₙ_real, range_cfcₙ_nnreal_subset, range_cfcₙ_subset	24
Total	24

(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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace 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.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring StarAlgHom.instFunLike cfcHom	—	cfcHom_mem_elemental
cfcHom_mem_elemental 📖	mathematical	—	StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing Ring.toSemiring SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace 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.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_le
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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing cfc 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	—	cfc_mem_elemental
cfc_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership 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	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SMulMemClass.ofIsScalarTower StarSubalgebra.topologicalClosure_minimal IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SubringClass.toSubsemiringClass cfc_mem_elemental
cfc_mem_elemental 📖	mathematical	—	StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing Ring.toSemiring SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing cfc 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	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfc_cases IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass StarSubalgebra.subsemiringClass cfcHom_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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing 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 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 IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMapZero.instStarRing RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalStarAlgHom.instFunLike cfcₙHom	—	cfcₙHom_mem_elemental
cfcₙHom_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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing 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 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 IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMapZero.instStarRing RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar range_cfcₙHom_le IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalStarAlgHom.instNonUnitalAlgHomClass
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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing 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	—	cfcₙ_mem_elemental
cfcₙ_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership 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	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SMulMemClass.ofIsScalarTower NonUnitalStarSubalgebra.topologicalClosure_minimal IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSubringClass.toNonUnitalSubsemiringClass cfcₙ_mem_elemental
cfcₙ_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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing 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	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_cases IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass ContinuousOn.restrict cfcₙHom_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 ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus SetLike.coe StarSubalgebra Ring.toSemiring StarSubalgebra.setLike StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RCLike.instContinuousStar Ring.toSemiring cfcHom ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMap.instStarModule StarMul.toStarModule StarAlgHom.range_eq_map_top ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace 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_cfcHom_le 📖	mathematical	—	StarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing Ring.toSemiring Preorder.toLE PartialOrder.toPreorder StarSubalgebra.instPartialOrder StarAlgHom.range ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring RCLike.instContinuousStar cfcHom StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMap.instStarModule StarMul.toStarModule StarAlgHom.range_eq_map_top ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace 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 le_imp_le_of_le_of_le StarSubalgebra.map_topologicalClosure_le cfcHom_continuous le_refl StarAlgHom.map_adjoin StarSubalgebra.topologicalClosure.congr_simp Set.image_singleton cfcHom_id instReflLe
range_cfc_nnreal 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.range cfc NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NNReal.instCommSemiring instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus 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 StarSubalgebra SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal subset_antisymm NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing Set.instAntisymmSubset range_cfc_nnreal_subset 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 em cfc_nonneg_iff Real.instStarOrderedRing instReflLe 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 Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NNReal.instCommSemiring 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 IsTopologicalRing.toIsSemitopologicalRing NNReal.coe_nonneg cfc_real_eq_nnreal
range_cfc_nnreal_subset 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set Set.instHasSubset Set.range cfc NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NNReal.instCommSemiring instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus setOf StarSubalgebra Real Real.instCommSemiring instStarRingReal SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing range_cfc_nnreal_eq_image_cfc_real Set.setOf_and SetLike.setOf_mem_eq Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar subset_refl Set.instReflSubset Set.inter_subset_inter range_cfc_subset LE.le.isSelfAdjoint Set.inter_comm Set.image_preimage_eq_inter_range Set.image_mono cfc_nonneg Real.instStarOrderedRing
range_cfc_subset 📖	mathematical	—	Set Set.instHasSubset 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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing range_cfc_eq_range_cfcHom Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset instIsConcreteLE range_cfcHom_le subset_refl Set.instReflSubset
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 NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass range_cfcₙ_eq_range_cfcₙHom 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 IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid 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 MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toNonUnitalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass cfcₙHom NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalStarAlgebra.elemental NonUnitalRing.toNonUnitalSemiring	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus ContinuousMapZero.instIsScalarTower' IsScalarTower.right ContinuousMapZero.instSMulCommClass' Algebra.to_smulCommClass ContinuousMapZero.instStarModule StarMul.toStarModule NonUnitalStarAlgebra.map_top instFactMemSetQuasispectrumOfNat NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum UniformContinuousConstSMul.to_continuousConstSMul 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ₙHom_le 📖	mathematical	—	NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder NonUnitalStarAlgHom.range 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 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 IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMapZero.instStarRing RCLike.toStarRing RCLike.instContinuousStar 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 MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toNonUnitalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass ContinuousMapZero.instIsScalarTower' IsScalarTower.right ContinuousMapZero.instSMulCommClass' Algebra.to_smulCommClass ContinuousMapZero.instStarModule StarMul.toStarModule NonUnitalStarAlgebra.map_top instFactMemSetQuasispectrumOfNat NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup ContinuousMapZero.instCStarRing RCLike.instCStarRing ContinuousMapZero.elemental_eq_top NonUnitalStarAlgebra.elemental.eq_1 le_imp_le_of_le_of_le NonUnitalStarSubalgebra.map_topologicalClosure_le cfcₙHom_continuous le_refl NonUnitalStarAlgHom.map_adjoin NonUnitalStarSubalgebra.topologicalClosure.congr_simp NonUnitalStarAlgebra.adjoin.congr_simp Set.image_singleton cfcₙHom_id instReflLe
range_cfcₙ_nnreal 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Set.range cfcₙ NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instCommSemiring NNReal.instNontrivial 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 NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus 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 NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgebra.elemental IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 instReflLe 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 Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instCommSemiring NNReal.instNontrivial 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 IsTopologicalRing.toIsSemitopologicalRing NNReal.coe_nonneg cfcₙ_real_eq_nnreal
range_cfcₙ_nnreal_subset 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Set Set.instHasSubset Set.range cfcₙ NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instCommSemiring NNReal.instNontrivial 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 IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing range_cfcₙ_nnreal_eq_image_cfcₙ_real Set.setOf_and SetLike.setOf_mem_eq Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar subset_refl Set.instReflSubset Set.inter_subset_inter range_cfcₙ_subset LE.le.isSelfAdjoint Set.inter_comm Set.image_preimage_eq_inter_range Set.image_mono cfcₙ_nonneg Real.instStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
range_cfcₙ_subset 📖	mathematical	—	Set Set.instHasSubset 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 IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsSemitopologicalRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass range_cfcₙ_eq_range_cfcₙHom Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset instIsConcreteLE range_cfcₙHom_le subset_refl Set.instReflSubset

---

← Back to Index