Isometric

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

Statistics

Metric	Count
Definitions IsometricContinuousFunctionalCalculus, NonUnitalIsometricContinuousFunctionalCalculus	2
Theorems nnnorm_cfc, nnnorm_cfc_nnreal, nnnorm_cfcₙ, nnnorm_cfcₙ_nnreal, norm_cfc, norm_cfcₙ, isGreatest_nnnorm_spectrum, isGreatest_norm_spectrum, isGreatest_spectrum, isometric, nnnorm_spectrum_le, norm_spectrum_le, spectrum_le, toContinuousFunctionalCalculus, toNonUnital, nnnorm_cfc, nnnorm_cfcₙ, isGreatest_nnnorm_quasispectrum, isGreatest_norm_quasispectrum, isGreatest_quasispectrum, isometric, nnnorm_quasispectrum_le, norm_quasispectrum_le, quasispectrum_le, toNonUnitalContinuousFunctionalCalculus, instIsometricContinuousFunctionalCalculus, instNonUnitalIsometricContinuousFunctionalCalculus, isometric_cfc, isometric_cfc, apply_le_nnnorm_cfc_nnreal, apply_le_nnnorm_cfcₙ_nnreal, isometry_cfcHom, isometry_cfcₙHom, nnnorm_apply_le_nnnorm_cfc, nnnorm_apply_le_nnnorm_cfcₙ, nnnorm_cfcHom, nnnorm_cfc_le, nnnorm_cfc_le_iff, nnnorm_cfc_lt, nnnorm_cfc_lt_iff, nnnorm_cfc_nnreal_le, nnnorm_cfc_nnreal_le_iff, nnnorm_cfc_nnreal_lt, nnnorm_cfc_nnreal_lt_iff, nnnorm_cfcₙHom, nnnorm_cfcₙ_le, nnnorm_cfcₙ_le_iff, nnnorm_cfcₙ_lt, nnnorm_cfcₙ_lt_iff, nnnorm_cfcₙ_nnreal_le, nnnorm_cfcₙ_nnreal_le_iff, nnnorm_cfcₙ_nnreal_lt, nnnorm_cfcₙ_nnreal_lt_iff, norm_apply_le_norm_cfc, norm_apply_le_norm_cfcₙ, norm_cfcHom, norm_cfc_le, norm_cfc_le_iff, norm_cfc_lt, norm_cfc_lt_iff, norm_cfcₙHom, norm_cfcₙ_le, norm_cfcₙ_le_iff, norm_cfcₙ_lt, norm_cfcₙ_lt_iff	65
Total	67

IsGreatest

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	IsGreatest NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus Set.image_image Set.image_congr norm_toNNReal Monotone.map_isGreatest Real.toNNReal_monotone norm_cfc
nnnorm_cfc_nnreal 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	IsGreatest instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus cfc_nnreal_eq_real NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Set.ext spectrum.algebraMap_mem NNReal.instIsScalarTowerOfReal IsScalarTower.left Real.toNNReal_coe NNReal.nnnorm_eq SpectrumRestricts.apply_mem SpectrumRestricts.eq_1 nnnorm_cfc Continuous.comp_continuousOn continuous_subtype_val ContinuousOn.comp Continuous.continuousOn continuous_real_toNNReal Set.mapsTo_image SpectrumRestricts.image IsSelfAdjoint.of_nonneg
nnnorm_cfcₙ 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	IsGreatest NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Set.image_image Set.image_congr norm_toNNReal Monotone.map_isGreatest Real.toNNReal_monotone norm_cfcₙ
nnnorm_cfcₙ_nnreal 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instZeroNNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	IsGreatest instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus cfcₙ_nnreal_eq_real NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Set.ext quasispectrum.algebraMap_mem IsScalarTower.left Real.toNNReal_coe NNReal.nnnorm_eq QuasispectrumRestricts.apply_mem nnnorm_cfcₙ Continuous.comp_continuousOn continuous_subtype_val ContinuousOn.comp Continuous.continuousOn continuous_real_toNNReal Set.mapsTo_image QuasispectrumRestricts.image Real.toNNReal_zero IsSelfAdjoint.of_nonneg
norm_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	IsGreatest Real Real.instLE Set.image Norm.norm NormedField.toNorm NormedRing.toNorm cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsCompact.exists_isGreatest instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsCompact.image_of_continuousOn ContinuousFunctionalCalculus.isCompact_spectrum ContinuousOn.norm Set.Nonempty.image ContinuousFunctionalCalculus.spectrum_nonempty ContinuousOn.restrict cfc_apply ContinuousFunctionalCalculus.compactSpace_spectrum norm_cfcHom le_antisymm ContinuousMap.norm_le norm_nonneg le_trans ContinuousMap.norm_coe_le_norm
norm_cfcₙ 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	IsGreatest Real Real.instLE Set.image Norm.norm NormedField.toNorm NonUnitalNormedRing.toNorm cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsCompact.exists_isGreatest instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsCompact.image_of_continuousOn NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum ContinuousOn.norm Set.Nonempty.image quasispectrum.nonempty IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousOn.restrict cfcₙ_apply NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum norm_cfcₙHom le_antisymm ContinuousMap.norm_le norm_nonneg le_trans ContinuousMap.norm_coe_le_norm

IsometricContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGreatest_nnnorm_spectrum 📖	mathematical	—	IsGreatest NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toContinuousFunctionalCalculus cfc_id IsGreatest.nnnorm_cfc continuousOn_id'
isGreatest_norm_spectrum 📖	mathematical	—	IsGreatest Real Real.instLE Set.image Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing NormedRing.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toContinuousFunctionalCalculus cfc_id IsGreatest.norm_cfc continuousOn_id'
isGreatest_spectrum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	IsGreatest NNReal instPartialOrderNNReal spectrum instCommSemiringNNReal NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus toContinuousFunctionalCalculus Set.image_congr Set.image_id' cfc_id IsGreatest.nnnorm_cfc_nnreal continuousOn_id'
isometric 📖	mathematical	—	Isometry ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace ContinuousMap.instMetricSpace ContinuousFunctionalCalculus.compactSpace_spectrum toContinuousFunctionalCalculus DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	—
nnnorm_spectrum_le 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toContinuousFunctionalCalculus cfc_id nnnorm_apply_le_nnnorm_cfc continuousOn_id'
norm_spectrum_le 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Real Real.instLE Norm.norm NormedField.toNorm NormedRing.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toContinuousFunctionalCalculus cfc_id norm_apply_le_norm_cfc continuousOn_id'
spectrum_le 📖	mathematical	NNReal Set Set.instMembership spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus toContinuousFunctionalCalculus cfc_id apply_le_nnnorm_cfc_nnreal continuousOn_id'
toContinuousFunctionalCalculus 📖	mathematical	—	ContinuousFunctionalCalculus UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	—
toNonUnital 📖	mathematical	—	NonUnitalIsometricContinuousFunctionalCalculus 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 NonUnitalNormedRing.toNonUnitalRing NormedRing.toNonUnitalNormedRing NormedRing.toMetricSpace NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing IsScalarTower.right Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra Algebra.to_smulCommClass	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital toContinuousFunctionalCalculus RCLike.toCompleteSpace ContinuousFunctionalCalculus.compactSpace_spectrum quasispectrum_eq_spectrum_union_zero IsCompact.union isCompact_singleton NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum IsDomain.toNontrivial instIsDomain IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul cfcₙHom_eq_cfcₙHom_of_cfcHom RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace cfcₙHom_of_cfcHom.eq_1 Isometry.comp isometry_cfcHom AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass spectrum_subset_quasispectrum continuous_inclusion le_antisymm ContinuousMapZero.instContinuousMapClass ContinuousMap.norm_le norm_nonneg ContinuousMap.norm_coe_le_norm Set.union_singleton map_zero ContinuousMapZero.instZeroHomClass norm_zero

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_cfc 📖	mathematical	MonotoneOn NNReal PartialOrder.toPreorder instPartialOrderNNReal spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing ContinuousOn NNReal.instTopologicalSpace Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsGreatest.unique NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsGreatest.nnnorm_cfc_nnreal map_isGreatest IsometricContinuousFunctionalCalculus.isGreatest_spectrum
nnnorm_cfcₙ 📖	mathematical	MonotoneOn NNReal PartialOrder.toPreorder instPartialOrderNNReal quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn NNReal.instTopologicalSpace instZeroNNReal Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsGreatest.unique NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsGreatest.nnnorm_cfcₙ_nnreal map_isGreatest NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum

NonUnitalIsometricContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGreatest_nnnorm_quasispectrum 📖	mathematical	—	IsGreatest NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.image NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalNormedRing.toNonUnitalSeminormedRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toNonUnitalContinuousFunctionalCalculus cfcₙ_id IsGreatest.nnnorm_cfcₙ continuousOn_id'
isGreatest_norm_quasispectrum 📖	mathematical	—	IsGreatest Real Real.instLE Set.image Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedRing.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toNonUnitalContinuousFunctionalCalculus cfcₙ_id IsGreatest.norm_cfcₙ continuousOn_id'
isGreatest_quasispectrum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	IsGreatest NNReal instPartialOrderNNReal quasispectrum instCommSemiringNNReal NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus toNonUnitalContinuousFunctionalCalculus Set.image_congr Set.image_id' cfcₙ_id IsGreatest.nnnorm_cfcₙ_nnreal continuousOn_id'
isometric 📖	mathematical	—	Isometry ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace ContinuousMapZero.instMetricSpace NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum toNonUnitalContinuousFunctionalCalculus DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	—
nnnorm_quasispectrum_le 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toNonUnitalContinuousFunctionalCalculus cfcₙ_id nnnorm_apply_le_nnnorm_cfcₙ continuousOn_id'
norm_quasispectrum_le 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing	Real Real.instLE Norm.norm NormedField.toNorm NonUnitalNormedRing.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar toNonUnitalContinuousFunctionalCalculus cfcₙ_id norm_apply_le_norm_cfcₙ continuousOn_id'
quasispectrum_le 📖	mathematical	NNReal Set Set.instMembership quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus toNonUnitalContinuousFunctionalCalculus cfcₙ_id apply_le_nnnorm_cfcₙ_nnreal continuousOn_id'
toNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	—

Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsometricContinuousFunctionalCalculus 📖	mathematical	—	IsometricContinuousFunctionalCalculus NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NormedRing.toMetricSpace NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal SpectrumRestricts.isometric_cfc NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.instCompleteSpace NNReal.instContinuousMap.UniqueHom NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isometry_subtype_coe le_rfl nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus Real.instCompleteSpace
instNonUnitalIsometricContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalIsometricContinuousFunctionalCalculus NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NonUnitalNormedRing.toMetricSpace NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal QuasispectrumRestricts.isometric_cfc NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.smulCommClass_left NNReal.instCompleteSpace NNReal.instContinuousMapZero.UniqueHom NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isometry_subtype_coe le_rfl nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometric_cfc 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing QuasispectrumRestricts ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instFunLike	NonUnitalIsometricContinuousFunctionalCalculus IsDomain.toNontrivial instIsDomain	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsDomain.toNontrivial instIsDomain cfc NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus EuclideanDomain.toNontrivial Isometry.isUniformEmbedding NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul cfcₙHom_eq_restrict Isometry.of_dist_eq Isometry.dist_eq isometry_cfcₙHom le_antisymm ContinuousMap.dist_le dist_nonneg ContinuousMap.dist_apply_le_dist quasispectrum.algebraMap_mem left_inv

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometric_cfc 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SpectrumRestricts ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instFunLike	IsometricContinuousFunctionalCalculus	—	cfc IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus Isometry.isUniformEmbedding ContinuousFunctionalCalculus.compactSpace_spectrum cfcHom_eq_restrict Isometry.of_dist_eq Isometry.dist_eq isometry_cfcHom le_antisymm ContinuousMap.dist_le dist_nonneg ContinuousMap.dist_apply_le_dist spectrum.algebraMap_mem QuasispectrumRestricts.left_inv

(root)

Definitions

Name	Category	Theorems
IsometricContinuousFunctionalCalculus 📖	CompData	4 math math: SpectrumRestricts.isometric_cfc, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, IsStarNormal.instIsometricContinuousFunctionalCalculus, Nonneg.instIsometricContinuousFunctionalCalculus
NonUnitalIsometricContinuousFunctionalCalculus 📖	CompData	5 math math: IsometricContinuousFunctionalCalculus.toNonUnital, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, QuasispectrumRestricts.isometric_cfc, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_le_nnnorm_cfc_nnreal 📖	mathematical	NNReal Set Set.instMembership spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing ContinuousOn NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus spectrum.of_subsingleton cfc.congr_simp IndiscreteTopology.nnnorm_eq_zero instIndiscreteTopologyOfSubsingleton NNReal.instCanonicallyOrderedAdd instIsEmptyFalse IsGreatest.nnnorm_cfc_nnreal
apply_le_nnnorm_cfcₙ_nnreal 📖	mathematical	NNReal Set Set.instMembership quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn NNReal.instTopologicalSpace instZeroNNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsGreatest.nnnorm_cfcₙ_nnreal
isometry_cfcHom 📖	mathematical	—	Isometry ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace ContinuousMap.instMetricSpace ContinuousFunctionalCalculus.compactSpace_spectrum IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	IsometricContinuousFunctionalCalculus.isometric
isometry_cfcₙHom 📖	mathematical	—	Isometry ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace ContinuousMapZero.instMetricSpace NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	NonUnitalIsometricContinuousFunctionalCalculus.isometric
nnnorm_apply_le_nnnorm_cfc 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_apply_le_norm_cfc
nnnorm_apply_le_nnnorm_cfcₙ 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsGreatest.nnnorm_cfcₙ
nnnorm_cfcHom 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing 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.toStarRing RCLike.instContinuousStar Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom SeminormedRing.toPseudoMetricSpace IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ContinuousMap.instSeminormedAddCommGroup ContinuousFunctionalCalculus.compactSpace_spectrum NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus ContinuousFunctionalCalculus.compactSpace_spectrum norm_cfcHom
nnnorm_cfc_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfc_le
nnnorm_cfc_le_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfc_le_iff
nnnorm_cfc_lt 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfc_lt
nnnorm_cfc_lt_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfc_lt_iff
nnnorm_cfc_nnreal_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus subsingleton_or_nontrivial nnnorm_zero NNReal.instCanonicallyOrderedAdd cfc_cases ContinuousOn.restrict cfc_apply isLUB_le_iff IsGreatest.isLUB IsGreatest.nnnorm_cfc_nnreal
nnnorm_cfc_nnreal_le_iff 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus LE.le.trans apply_le_nnnorm_cfc_nnreal nnnorm_cfc_nnreal_le
nnnorm_cfc_nnreal_lt 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus subsingleton_or_nontrivial nnnorm_zero cfc_cases ContinuousOn.restrict cfc_apply IsGreatest.lt_iff IsGreatest.nnnorm_cfc_nnreal
nnnorm_cfc_nnreal_lt_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal ContinuousOn NNReal.instTopologicalSpace spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus LE.le.trans_lt apply_le_nnnorm_cfc_nnreal nnnorm_cfc_nnreal_lt
nnnorm_cfcₙHom 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule 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 NonUnitalStarAlgHom.instFunLike cfcₙHom NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing ContinuousMapZero.instNonUnitalNormedCommRing NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum norm_cfcₙHom
nnnorm_cfcₙ_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NormedSpace.toModule NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfcₙ_le
nnnorm_cfcₙ_le_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfcₙ_le_iff
nnnorm_cfcₙ_lt 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NormedSpace.toModule NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfcₙ_lt
nnnorm_cfcₙ_lt_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfcₙ_lt_iff
nnnorm_cfcₙ_nnreal_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_cases NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus nnnorm_zero NNReal.instCanonicallyOrderedAdd ContinuousOn.restrict IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul cfcₙ_apply isLUB_le_iff IsGreatest.isLUB IsGreatest.nnnorm_cfcₙ_nnreal
nnnorm_cfcₙ_nnreal_le_iff 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instZeroNNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus LE.le.trans apply_le_nnnorm_cfcₙ_nnreal nnnorm_cfcₙ_nnreal_le
nnnorm_cfcₙ_nnreal_lt 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_cases NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus nnnorm_zero LE.le.trans_lt zero_le NNReal.instCanonicallyOrderedAdd quasispectrum.zero_mem ContinuousOn.restrict IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul cfcₙ_apply IsGreatest.lt_iff IsGreatest.nnnorm_cfcₙ_nnreal
nnnorm_cfcₙ_nnreal_lt_iff 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instZeroNNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Preorder.toLT instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup 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 NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus LE.le.trans_lt apply_le_nnnorm_cfcₙ_nnreal nnnorm_cfcₙ_nnreal_lt
norm_apply_le_norm_cfc 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	Real Real.instLE Norm.norm NormedField.toNorm NormedRing.toNorm cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus spectrum.of_subsingleton norm_of_subsingleton instIsEmptyFalse IsGreatest.norm_cfc
norm_apply_le_norm_cfcₙ 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	Real Real.instLE Norm.norm NormedField.toNorm NonUnitalNormedRing.toNorm cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsGreatest.norm_cfcₙ
norm_cfcHom 📖	mathematical	—	Norm.norm NormedRing.toNorm DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing 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.toStarRing RCLike.instContinuousStar Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom SeminormedRing.toPseudoMetricSpace IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ContinuousMap.instNorm ContinuousFunctionalCalculus.compactSpace_spectrum NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Isometry.norm_map_of_map_zero ContinuousFunctionalCalculus.compactSpace_spectrum IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus isometry_cfcHom map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass
norm_cfc_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NormedRing.toNorm cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus subsingleton_or_nontrivial norm_zero cfc_cases ContinuousOn.restrict cfc_apply isLUB_le_iff IsGreatest.isLUB IsGreatest.norm_cfc
norm_cfc_le_iff 📖	mathematical	Real Real.instLE Real.instZero ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Norm.norm NormedRing.toNorm cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace NormedField.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus LE.le.trans norm_apply_le_norm_cfc norm_cfc_le
norm_cfc_lt 📖	mathematical	Real Real.instLT Real.instZero Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NormedRing.toNorm cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus subsingleton_or_nontrivial norm_zero cfc_cases ContinuousOn.restrict cfc_apply IsGreatest.lt_iff IsGreatest.norm_cfc
norm_cfc_lt_iff 📖	mathematical	Real Real.instLT Real.instZero ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Norm.norm NormedRing.toNorm cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace NormedField.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus LE.le.trans_lt norm_apply_le_norm_cfc norm_cfc_lt
norm_cfcₙHom 📖	mathematical	—	Norm.norm NonUnitalNormedRing.toNorm DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing 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 NonUnitalStarAlgHom.instFunLike cfcₙHom NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ContinuousMapZero.instNorm NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Isometry.norm_map_of_map_zero NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul isometry_cfcₙHom map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass
norm_cfcₙ_le 📖	mathematical	Real Real.instLE Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNorm cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_cases NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus norm_zero LE.le.trans norm_nonneg quasispectrum.zero_mem ContinuousOn.restrict IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul cfcₙ_apply isLUB_le_iff IsGreatest.isLUB IsGreatest.norm_cfcₙ
norm_cfcₙ_le_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	Real Real.instLE Norm.norm NonUnitalNormedRing.toNorm cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace NormedField.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus LE.le.trans norm_apply_le_norm_cfcₙ norm_cfcₙ_le
norm_cfcₙ_lt 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalNormedRing.toNorm cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField 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 NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_cases NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus norm_zero LE.le.trans_lt norm_nonneg quasispectrum.zero_mem ContinuousOn.restrict IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul cfcₙ_apply IsGreatest.lt_iff IsGreatest.norm_cfcₙ
norm_cfcₙ_lt_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	Real Real.instLT Norm.norm NonUnitalNormedRing.toNorm cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace NormedField.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus LE.le.trans_lt norm_apply_le_norm_cfcₙ norm_cfcₙ_lt

---

← Back to Index