NonUnital

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

Statistics

Metric	Count
Definitions UniqueHom, NonUnitalClosedEmbeddingContinuousFunctionalCalculus, NonUnitalContinuousFunctionalCalculus, cfcₙ, cfcₙHom, cfcₙHomSuperset, cfcₙHom_of_cfcHom, cfcₙL	8
Theorems eq_zero_of_quasispectrum_eq_zero, quasispectrum_zero_eq, toNonUnital, toNonUnital, eq_of_continuous_of_map_id, cfcₙ, cfcₙ_map, isClosedEmbedding, toNonUnitalContinuousFunctionalCalculus, compactSpace_quasispectrum, exists_cfc_of_predicate, isCompact_quasispectrum, predicate_zero, ext_continuousMap, nonneg_iff_quasispectrum_nonneg, cfcₙHomSuperset_apply, cfcₙHomSuperset_continuous, cfcₙHomSuperset_id, cfcₙHom_comp, cfcₙHom_continuous, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_eq_cfcₙ_extend, cfcₙHom_eq_of_continuous_of_map_id, cfcₙHom_id, cfcₙHom_injective, cfcₙHom_isClosedEmbedding, cfcₙHom_le_iff, cfcₙHom_map_quasispectrum, cfcₙHom_mono, cfcₙHom_nonneg_iff, cfcₙHom_of_cfcHom_injective, cfcₙHom_of_cfcHom_map_quasispectrum, cfcₙHom_predicate, cfcₙL_apply, cfcₙ_add, cfcₙ_apply, cfcₙ_apply_mkD, cfcₙ_apply_of_not_and_and, cfcₙ_apply_of_not_continuousOn, cfcₙ_apply_of_not_map_zero, cfcₙ_apply_of_not_predicate, cfcₙ_apply_pi, cfcₙ_apply_zero, cfcₙ_cases, cfcₙ_commute_cfcₙ, cfcₙ_comp, cfcₙ_comp', cfcₙ_comp_const_mul, cfcₙ_comp_neg, cfcₙ_comp_smul, cfcₙ_comp_star, cfcₙ_congr, cfcₙ_const_mul, cfcₙ_const_mul_id, cfcₙ_const_zero, cfcₙ_def, cfcₙ_eq_cfc, cfcₙ_eq_cfcₙL, cfcₙ_eq_cfcₙL_mkD, cfcₙ_eq_cfcₙ_iff_eqOn, cfcₙ_id, cfcₙ_id', cfcₙ_le_iff, cfcₙ_map_quasispectrum, cfcₙ_mono, cfcₙ_mul, cfcₙ_neg, cfcₙ_neg_id, cfcₙ_nonneg, cfcₙ_nonneg_iff, cfcₙ_nonneg_of_predicate, cfcₙ_nonpos, cfcₙ_nonpos_iff, cfcₙ_predicate, cfcₙ_predicate_zero, cfcₙ_smul, cfcₙ_smul_id, cfcₙ_star, cfcₙ_star_id, cfcₙ_sub, cfcₙ_sum, cfcₙ_sum_univ, cfcₙ_zero, continuous_cfcₙHom_of_cfcHom, eqOn_of_cfcₙ_eq_cfcₙ, instFactMemSetQuasispectrumOfNat, isClosedEmbedding_cfcₙHom_of_cfcHom, range_cfcₙ_eq_range_cfcₙHom	88
Total	96

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_quasispectrum_eq_zero 📖	mathematical	Set Set.instHasSubset quasispectrum Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_id cfcₙ_const_zero cfcₙ_congr
quasispectrum_zero_eq 📖	mathematical	—	quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set Set.instSingletonSet NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Set.eq_singleton_iff_unique_mem quasispectrum.zero_mem Set.image_congr cfcₙ_map_quasispectrum Continuous.continuousOn continuous_zero cfcₙ_predicate_zero cfcₙ_zero

ClosedEmbeddingContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNonUnital 📖	mathematical	—	NonUnitalClosedEmbeddingContinuousFunctionalCalculus Semifield.toCommSemiring IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring IsScalarTower.right Algebra.to_smulCommClass	—	IsScalarTower.right Algebra.to_smulCommClass IsDomain.toNontrivial instIsDomain ContinuousFunctionalCalculus.toNonUnital toContinuousFunctionalCalculus IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙHom_eq_cfcₙHom_of_cfcHom isClosedEmbedding_cfcₙHom_of_cfcHom

ContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNonUnital 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus Semifield.toCommSemiring IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring IsScalarTower.right Algebra.to_smulCommClass	—	IsDomain.toNontrivial instIsDomain IsScalarTower.right Algebra.to_smulCommClass cfc_predicate_zero compactSpace_spectrum quasispectrum_eq_spectrum_union_zero IsCompact.union isCompact_singleton IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul continuous_cfcₙHom_of_cfcHom cfcₙHom_of_cfcHom_injective cfcHom_id cfcₙHom_of_cfcHom_map_quasispectrum cfcHom_predicate

ContinuousMapZero

Definitions

Name	Category	Theorems
UniqueHom 📖	CompData	2 math math: RCLike.uniqueNonUnitalContinuousFunctionalCalculus, NNReal.instContinuousMapZero.UniqueHom

ContinuousMapZero.UniqueHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_continuous_of_map_id 📖	—	Continuous ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike ContinuousMapZero.id	—	—	—

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcₙ 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid cfcₙ	—	cfcₙ_predicate

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcₙ_map 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid cfcₙ	—	cfcₙ_cases Commute.zero_right ContinuousOn.restrict IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙ_apply cfcₙ_star cfcₙ_mul ContinuousOn.star star_zero mul_comm

NonUnitalClosedEmbeddingContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding 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 ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom toNonUnitalContinuousFunctionalCalculus	—	—
toNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus	—	—

NonUnitalContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_quasispectrum 📖	mathematical	—	CompactSpace Set.Elem quasispectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	—
exists_cfc_of_predicate 📖	mathematical	—	NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Continuous ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom.instFunLike ContinuousMap.restrict ContinuousMap.id ContinuousMap ContinuousMap.instFunLike Set.range ContinuousMapZero.instFunLike	—	—
isCompact_quasispectrum 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum	—	isCompact_iff_compactSpace compactSpace_quasispectrum
predicate_zero 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	—

NonUnitalStarAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_continuousMap 📖	—	Continuous 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 ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing instFunLike ContinuousMapZero.id instFactMemSetQuasispectrumOfNat	—	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul instFactMemSetQuasispectrumOfNat ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id

StarOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonneg_iff_quasispectrum_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	cfcₙ_nonneg_iff continuousOn_id' cfcₙ_id

(root)

Definitions

Name	Category	Theorems
NonUnitalClosedEmbeddingContinuousFunctionalCalculus 📖	CompData	5 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, ClosedEmbeddingContinuousFunctionalCalculus.toNonUnital, QuasispectrumRestricts.nonUnitalClosedEmbeddingCFC, RCLike.nonUnitalContinuousFunctionalCalculusIsClosedEmbedding, instNonUnitalClosedEmbeddingContinuousFunctionalCalculusOfCompleteSpace
NonUnitalContinuousFunctionalCalculus 📖	CompData	7 math math: RCLike.nonUnitalContinuousFunctionalCalculus, ContinuousFunctionalCalculus.toNonUnital, IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus, NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus, Nonneg.instNonUnitalContinuousFunctionalCalculus, QuasispectrumRestricts.cfc, NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus
cfcₙ 📖	CompOp	156 math math: range_cfcₙ_nnreal, integrableOn_cfcₙ', cfcₙ_def, cfcₙ_norm_nonneg, ContinuousWithinAt.cfcₙ, CFC.monotoneOn_one_sub_one_add_inv, cfcₙ_zero, nnnorm_cfcₙ_nnreal_le_iff, cfcₙ_const_zero, Commute.cfcₙ_nnreal, Continuous.cfcₙ_fun, Unitization.real_cfcₙ_eq_cfc_inr, CFC.abs_eq_cfcₙ_coe_norm, QuasispectrumRestricts.cfcₙ_eq_restrict, nnnorm_cfcₙ_lt_iff, ContinuousOn.cfcₙ', IsGreatest.nnnorm_cfcₙ, cfcₙ_sub, cfcₙ_map_pi, NonUnitalStarAlgHom.map_cfcₙ, cfcₙ_eq_cfcₙL_mkD, cfcₙ_integral, tendsto_cfcₙ_fun, cfcₙ_setIntegral, cfcₙ_apply_mkD, cfcₙ_eq_cfc, IsStarNormal.cfcₙ_map, cfcₙ_comp, norm_cfcₙ_lt, cfcₙ_apply_zero, IsGreatest.norm_cfcₙ, nnnorm_cfcₙ_nnreal_lt, cfcₙ_re_id, cfcₙ_comp_norm, cfcₙ_neg, cfcₙ_apply_of_not_map_zero, Continuous.cfcₙ_of_mem_nhdsSet, Continuous.cfcₙ, continuousOn_cfcₙ, range_cfcₙ, cfcₙ_sum_univ, IsGreatest.nnnorm_cfcₙ_nnreal, cfcₙ_mem_elemental, nnnorm_apply_le_nnnorm_cfcₙ, cfcₙ_real_eq_complex, CFC.nnrpow_def, cfcₙ_apply_of_not_predicate, cfcₙ_comp_re, integrable_cfcₙ, cfcₙ_add, norm_cfcₙ_lt_iff, cfcₙ_neg_id, cfcₙ_comp_im, Continuous.cfcₙ_nnreal, cfcₙ_nonpos, cfcₙ_comp_neg, ContinuousAt.cfcₙ_nnreal, range_cfcₙ_eq_range_cfcₙHom, Filter.Tendsto.cfcₙ, cfcₙ_predicate, cfcₙ_tsub, CFC.monotoneOn_one_sub_one_add_inv_real, ContinuousWithinAt.cfcₙ_nnreal, range_cfcₙ_nnreal_eq_image_cfcₙ_real, Filter.Tendsto.cfcₙ_nnreal, lipschitzOnWith_cfcₙ_fun, nnnorm_cfcₙ_nnreal_lt_iff, cfcₙ_imaginaryPart, cfcₙ_real_eq_nnreal, cfcₙ_map_prod, ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, cfcₙHom_eq_cfcₙ_extend, cfcₙ_comp_smul, cfcₙ_mem, cfcₙ_id, cfcₙ_im_id, cfcₙ_eq_cfcₙ_iff_eqOn, ContinuousOn.cfcₙ_fun, cfcₙ_congr, integrableOn_cfcₙ, norm_cfcₙ_le, cfcₙ_id', ContinuousOn.cfcₙ_nnreal', integrable_cfcₙ', Unitization.nnreal_cfcₙ_eq_cfc_inr, range_cfcₙ_subset, cfcₙ_mul, Continuous.cfcₙ_nnreal_of_mem_nhdsSet, ContinuousOn.cfcₙ, NonUnitalStarAlgHomClass.map_cfcₙ, lipschitzOnWith_cfcₙ_fun_of_subset, cfcₙ_sum, ContinuousOn.cfcₙ_of_mem_nhdsSet, range_cfcₙ_nnreal_subset, CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, cfcₙ_mono, Continuous.cfcₙ', cfcₙ_norm_sq_nonneg, Commute.cfcₙ, cfcₙ_comp', ContinuousAt.cfcₙ, nnnorm_cfcₙ_le_iff, norm_cfcₙ_one_sub_one_add_inv_lt_one, CFC.abs_eq_cfcₙ_norm, continuousOn_cfcₙ_nnreal, continuousWithinAt_cfcₙ_fun, cfcₙ_apply_pi, continuousOn_cfcₙ_setProd, Unitization.complex_cfcₙ_eq_cfc_inr, cfcₙ_star, cfcₙ_nnreal_eq_real, CFC.nnrpow_eq_cfcₙ_real, cfcₙ_apply_of_not_and_and, cfcₙ_nonneg_iff, CFC.negPart_def, cfcₙ_nonpos_iff, cfcₙ_realPart, cfcₙ_eq_cfcₙL, cfcₙ_setIntegral', ContinuousOn.cfcₙ_nnreal, cfcₙ_apply_mem_elemental, CFC.posPart_def, CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one, IsSelfAdjoint.commute_cfcₙ, norm_apply_le_norm_cfcₙ, cfcₙ_const_mul, cfcₙ_cases, cfcₙ_star_id, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, cfcₙ_smul, cfcₙ_nonneg, nnnorm_cfcₙ_le, cfcₙ_apply, nnnorm_cfcₙ_nnreal_le, CFC.sqrt_eq_real_sqrt, apply_le_nnnorm_cfcₙ_nnreal, cfcₙ_comp_star, cfcₙ_map_quasispectrum, cfcₙ_comp_const_mul, continuousOn_cfcₙ_nnreal_setProd, MonotoneOn.nnnorm_cfcₙ, cfcₙ_commute_cfcₙ, cfcₙ_const_mul_id, norm_cfcₙ_le_iff, cfcₙ_smul_id, Commute.cfcₙ_real, cfcₙ_complex_eq_real, cfcₙ_le_iff, cfcₙ_apply_of_not_continuousOn, Continuous.cfcₙ_nnreal', cfcₙ_nonneg_of_predicate, continuousAt_cfcₙ_fun, Unitization.cfcₙ_eq_cfc_inr, cfcₙ_integral', IsSelfAdjoint.cfcₙ, nnnorm_cfcₙ_lt
cfcₙHom 📖	CompOp	37 math math: cfcₙ_def, norm_cfcₙHom, cfcₙHom_mono, NonUnitalIsometricContinuousFunctionalCalculus.isometric, cfcₙHom_apply_mem_elemental, cfcₙHom_nnreal_eq_restrict, cfcₙHom_mem_elemental, cfcₙ_apply_mkD, cfcₙHom_id, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, range_cfcₙHom, NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding, QuasispectrumRestricts.cfcₙHom_eq_restrict, cfcₙHom_integral, isometry_cfcₙHom, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_predicate, cfcₙHom_comp, Commute.cfcₙHom, range_cfcₙ_eq_range_cfcₙHom, range_cfcₙHom_le, inr_comp_cfcₙHom_eq_cfcₙAux, cfcₙHom_isClosedEmbedding, cfcₙHom_le_iff, cfcₙHom_eq_cfcₙ_extend, cfcₙHom_map_quasispectrum, cfcₙHom_injective, cfcₙHom_real_eq_restrict, nnnorm_cfcₙHom, IsSelfAdjoint.commute_cfcₙHom, cfcₙHom_continuous, cfcₙ_apply_pi, cfcₙL_apply, cfcₙHomSuperset_apply, cfcₙ_apply, cfcₙHom_nonneg_iff, cfcₙHom_eq_of_continuous_of_map_id
cfcₙHomSuperset 📖	CompOp	4 math math: continuous_cfcₙHomSuperset_left, cfcₙHomSuperset_id, cfcₙHomSuperset_continuous, cfcₙHomSuperset_apply
cfcₙHom_of_cfcHom 📖	CompOp	5 math math: cfcₙHom_of_cfcHom_injective, cfcₙHom_eq_cfcₙHom_of_cfcHom, continuous_cfcₙHom_of_cfcHom, isClosedEmbedding_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom_map_quasispectrum
cfcₙL 📖	CompOp	5 math math: cfcₙL_integral, cfcₙ_eq_cfcₙL_mkD, cfcₙ_eq_cfcₙL, cfcₙL_apply, cfcₙL_integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcₙHomSuperset_apply 📖	mathematical	Set Set.instHasSubset quasispectrum	DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set Set.instMembership quasispectrum.zero_mem instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHomSuperset quasispectrum quasispectrum.instZero cfcₙHom ContinuousMapZero.comp Subtype.map	—	quasispectrum.zero_mem IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul
cfcₙHomSuperset_continuous 📖	mathematical	Set Set.instHasSubset quasispectrum	Continuous ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set Set.instMembership quasispectrum.zero_mem instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHomSuperset	—	quasispectrum.zero_mem Continuous.comp IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙHom_continuous ContinuousMapZero.continuous_precomp
cfcₙHomSuperset_id 📖	mathematical	Set Set.instHasSubset quasispectrum	DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set Set.instMembership quasispectrum.zero_mem instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHomSuperset ContinuousMapZero.id	—	cfcₙHom_id
cfcₙHom_comp 📖	mathematical	DFunLike.coe 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 ContinuousMapZero.instFunLike NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom ContinuousMapZero.comp cfcₙHom_predicate	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙHom_predicate cfcₙHom_eq_of_continuous_of_map_id Continuous.comp cfcₙHom_continuous ContinuousMapZero.instContinuousMapClass continuous_induced_rng ContinuousMap.continuous_precomp continuous_induced_dom instFactMemSetQuasispectrumOfNat ContinuousMapZero.ext DFunLike.congr_fun
cfcₙHom_continuous 📖	mathematical	—	Continuous 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 ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcₙHom_eq_cfcₙHom_of_cfcHom 📖	mathematical	—	cfcₙHom Semifield.toCommSemiring IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital cfcₙHom_of_cfcHom	—	IsScalarTower.right Algebra.to_smulCommClass cfcₙHom_eq_of_continuous_of_map_id IsDomain.toNontrivial instIsDomain ContinuousFunctionalCalculus.toNonUnital continuous_cfcₙHom_of_cfcHom cfcHom_id
cfcₙHom_eq_cfcₙ_extend 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom cfcₙ Function.extend ContinuousMapZero.instFunLike	—	Function.Injective.extend_apply continuousOn_iff_continuous_restrict ContinuousMapClass.map_continuous ContinuousMapZero.instContinuousMapClass quasispectrum.coe_zero Subtype.val_injective map_zero ContinuousMapZero.instZeroHomClass IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply ContinuousMap.continuous_toFun ContinuousMapZero.map_zero'
cfcₙHom_eq_of_continuous_of_map_id 📖	mathematical	Continuous 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 ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike ContinuousMapZero.id instFactMemSetQuasispectrumOfNat	cfcₙHom	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul instFactMemSetQuasispectrumOfNat NonUnitalStarAlgHom.ext_continuousMap NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum cfcₙHom_continuous cfcₙHom_id
cfcₙHom_id 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom ContinuousMapZero.id instFactMemSetQuasispectrumOfNat	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcₙHom_injective 📖	mathematical	—	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 DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcₙHom_isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding 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 ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus	—	NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding
cfcₙHom_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum CommRing.toCommSemiring quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom ContinuousMapZero.instPartialOrder	—	IsTopologicalRing.toIsTopologicalSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙHom_nonneg_iff IsSemitopologicalRing.toIsSemitopologicalSemiring ContinuousMapZero.instStarOrderedRing ContinuousMap.instStarOrderedRingOfContinuousSqrt
cfcₙHom_map_quasispectrum 📖	mathematical	—	quasispectrum DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom Set.range ContinuousMapZero.instFunLike	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcₙHom_mono 📖	mathematical	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 Preorder.toLE PartialOrder.toPreorder ContinuousMapZero.instPartialOrder	Preorder.toLE PartialOrder.toPreorder DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	OrderHomClass.mono IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul StarRingHomClass.instOrderHomClass ContinuousMapZero.instStarOrderedRing ContinuousMap.instStarOrderedRingOfContinuousSqrt NonUnitalAlgHomClass.toNonUnitalRingHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass NonUnitalStarAlgHom.instStarHomClass
cfcₙHom_nonneg_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalStarAlgHom.instFunLike cfcₙHom ContinuousMapZero.instPartialOrder ContinuousMapZero.instZero	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg cfcₙHom_map_quasispectrum map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙHom_mono
cfcₙHom_of_cfcHom_injective 📖	mathematical	—	ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring quasispectrum.instZero IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom_of_cfcHom	—	IsDomain.toNontrivial instIsDomain cfcHom_injective ContinuousMapZero.ext eq_or_ne map_zero ContinuousMapZero.instZeroHomClass quasispectrum_eq_spectrum_union_zero Set.union_singleton Subtype.prop Subtype.val_injective
cfcₙHom_of_cfcHom_map_quasispectrum 📖	mathematical	—	quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum.instZero IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom_of_cfcHom Set.range ContinuousMapZero.instFunLike	—	IsDomain.toNontrivial instIsDomain IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul quasispectrum_eq_spectrum_union_zero cfcHom_map_spectrum Set.ext spectrum_subset_quasispectrum map_zero ContinuousMapZero.instZeroHomClass Subtype.val_injective
cfcₙHom_predicate 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcₙL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.funLike cfcₙL NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalStarAlgHom.instFunLike cfcₙHom	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul
cfcₙ_add 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply ContinuousOn.fun_add add_zero SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙ_apply_of_not_predicate
cfcₙ_apply 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom Set.restrict ContinuousOn.restrict	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_def
cfcₙ_apply_mkD 📖	mathematical	—	cfcₙ DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom ContinuousMapZero.mkD Set.restrict ContinuousMapZero.instZero	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply ContinuousMapZero.mkD_of_continuousOn cfcₙ_apply_of_not_map_zero ContinuousMapZero.mkD_of_not_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙ_apply_of_not_continuousOn ContinuousMapZero.mkD_of_not_continuousOn
cfcₙ_apply_of_not_and_and 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_def
cfcₙ_apply_of_not_continuousOn 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_def
cfcₙ_apply_of_not_map_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_def
cfcₙ_apply_of_not_predicate 📖	mathematical	—	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_def
cfcₙ_apply_pi 📖	mathematical	—	cfcₙ DFunLike.coe NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom Set.restrict ContinuousOn.restrict	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply
cfcₙ_apply_zero 📖	mathematical	—	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_zero cfcₙ_congr CFC.quasispectrum_zero_eq cfcₙ_apply_of_not_map_zero
cfcₙ_cases 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalStarAlgHom.instFunLike cfcₙHom Set.restrict ContinuousOn.restrict	cfcₙ	—	ContinuousOn.restrict IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙ_apply cfcₙ_apply_of_not_continuousOn cfcₙ_apply_of_not_map_zero cfcₙ_apply_of_not_predicate
cfcₙ_commute_cfcₙ 📖	mathematical	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ	—	cfcₙ_cases ContinuousOn.restrict IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Commute.map NonUnitalAlgSemiHomClass.toMulHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass Commute.all
cfcₙ_comp 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ	—	ContinuousOn.comp Set.mapsTo_image IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙHom_map_quasispectrum Set.ext Set.range_restrict cfcₙ_apply cfcₙHom_predicate Continuous.codRestrict cfcₙHom_comp
cfcₙ_comp' 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ	—	cfcₙ_comp
cfcₙ_comp_const_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	cfcₙ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	cfcₙ_comp' ContinuousOn.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring continuousOn_id' MulZeroClass.mul_zero cfcₙ_const_mul_id
cfcₙ_comp_neg 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing quasispectrum CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring cfcₙ_comp' ContinuousOn.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing continuousOn_id' neg_zero cfcₙ_neg_id
cfcₙ_comp_smul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring quasispectrum	cfcₙ SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_comp' ContinuousOn.const_smul continuousOn_id' smul_zero cfcₙ_smul_id
cfcₙ_comp_star 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	cfcₙ Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_comp' ContinuousOn.star continuousOn_id' star_zero cfcₙ_star_id
cfcₙ_congr 📖	mathematical	Set.EqOn quasispectrum	cfcₙ	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict ContinuousOn.congr quasispectrum.zero_mem cfcₙ_apply Set.restrict_eq_iff cfcₙ_apply_of_not_predicate cfcₙ_apply_of_not_continuousOn Set.EqOn.symm cfcₙ_apply_of_not_map_zero
cfcₙ_const_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	cfcₙ_smul SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring IsScalarTower.left Pi.isScalarTower IsScalarTower.right
cfcₙ_const_mul_id 📖	mathematical	—	cfcₙ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	cfcₙ_smul_id SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring IsScalarTower.left Pi.isScalarTower IsScalarTower.right
cfcₙ_const_zero 📖	mathematical	—	cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_zero
cfcₙ_def 📖	mathematical	—	cfcₙ ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum.instZero instTopologicalSpaceSubtype Set Set.instMembership MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ContinuousMapZero.instModule Semiring.toModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom Set.restrict	—	—
cfcₙ_eq_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	cfcₙ Semifield.toCommSemiring IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital cfc	—	IsScalarTower.right Algebra.to_smulCommClass IsDomain.toNontrivial instIsDomain ContinuousFunctionalCalculus.toNonUnital ContinuousOn.mono spectrum_subset_quasispectrum ContinuousOn.restrict cfc_apply IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙ_apply cfcₙHom_eq_cfcₙHom_of_cfcHom cfcₙHom_of_cfcHom.eq_1 cfcₙ_apply_of_not_predicate cfc_apply_of_not_predicate
cfcₙ_eq_cfcₙL 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.funLike cfcₙL Set.restrict ContinuousOn.restrict	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_def cfcₙL_apply
cfcₙ_eq_cfcₙL_mkD 📖	mathematical	—	cfcₙ DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.funLike cfcₙL ContinuousMapZero.mkD Set.restrict ContinuousMapZero.instZero	—	cfcₙ_apply_mkD
cfcₙ_eq_cfcₙ_iff_eqOn 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ Set.EqOn quasispectrum	—	eqOn_of_cfcₙ_eq_cfcₙ cfcₙ_congr
cfcₙ_id 📖	mathematical	—	cfcₙ	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict continuousOn_id' cfcₙHom_id cfcₙ_apply
cfcₙ_id' 📖	mathematical	—	cfcₙ	—	cfcₙ_id
cfcₙ_le_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Preorder.toLE PartialOrder.toPreorder cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicalRing.toIsTopologicalSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply cfcₙHom_le_iff ContinuousMapZero.le_def
cfcₙ_map_quasispectrum 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	quasispectrum cfcₙ Set.image	—	ContinuousOn.restrict IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙ_apply cfcₙHom_map_quasispectrum Set.range_restrict
cfcₙ_mono 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Preorder.toLE PartialOrder.toPreorder cfcₙ	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply cfcₙHom_mono cfcₙ_apply_of_not_predicate
cfcₙ_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply IsTopologicalSemiring.toContinuousMul map_mul NonUnitalAlgSemiHomClass.toMulHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass ContinuousOn.fun_mul MulZeroClass.mul_zero cfcₙ_apply_of_not_predicate
cfcₙ_neg 📖	mathematical	—	cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass ContinuousOn.neg IsSemitopologicalRing.toContinuousNeg neg_zero cfcₙ_apply_of_not_predicate cfcₙ_apply_of_not_continuousOn neg_neg cfcₙ_apply_of_not_map_zero neg_eq_zero
cfcₙ_neg_id 📖	mathematical	—	cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring cfcₙ_neg cfcₙ_id'
cfcₙ_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ	—	cfcₙ_const_zero cfcₙ_mono continuousOn_const cfcₙ_apply_of_not_continuousOn cfcₙ_apply_of_not_map_zero
cfcₙ_nonneg_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply cfcₙHom_nonneg_iff ContinuousMapZero.le_def
cfcₙ_nonneg_of_predicate 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ	—	cfcₙ_predicate
cfcₙ_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Preorder.toLE PartialOrder.toPreorder cfcₙ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_const_zero cfcₙ_mono continuousOn_const cfcₙ_apply_of_not_continuousOn cfcₙ_apply_of_not_map_zero
cfcₙ_nonpos_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Preorder.toLE PartialOrder.toPreorder cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid cfcₙ_nonneg_iff ContinuousOn.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing neg_zero
cfcₙ_predicate 📖	mathematical	—	cfcₙ	—	cfcₙ_cases cfcₙ_predicate_zero ContinuousOn.restrict cfcₙHom_predicate
cfcₙ_predicate_zero 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	NonUnitalContinuousFunctionalCalculus.predicate_zero
cfcₙ_smul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply ContinuousOn.const_smul smul_zero smul_one_smul map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙ_apply_of_not_predicate
cfcₙ_smul_id 📖	mathematical	—	cfcₙ SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_smul continuousOn_id' cfcₙ_id'
cfcₙ_star 📖	mathematical	—	cfcₙ Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply StarHomClass.map_star NonUnitalStarAlgHom.instStarHomClass ContinuousOn.star star_zero cfcₙ_apply_of_not_predicate cfcₙ_apply_of_not_continuousOn star_star cfcₙ_apply_of_not_map_zero
cfcₙ_star_id 📖	mathematical	—	cfcₙ Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_star cfcₙ_id'
cfcₙ_sub 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	cfcₙ CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub sub_self cfcₙ_apply_of_not_predicate
cfcₙ_sum 📖	mathematical	—	cfcₙ Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Finset.sum_apply Finset.sum_coe_sort continuousOn_finset_sum IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict cfcₙ_apply_pi map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass Finset.sum_congr Finset.sum_const_zero cfcₙ_apply ContinuousMapZero.ext ContinuousMapZero.coe_sum cfcₙ_apply_of_not_predicate
cfcₙ_sum_univ 📖	mathematical	—	cfcₙ Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.univ NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	cfcₙ_sum
cfcₙ_zero 📖	mathematical	—	cfcₙ Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousOn.restrict Continuous.continuousOn continuous_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass cfcₙ_apply cfcₙ_apply_of_not_predicate
continuous_cfcₙHom_of_cfcHom 📖	mathematical	—	Continuous ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring quasispectrum.instZero IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom_of_cfcHom	—	Continuous.comp IsDomain.toNontrivial instIsDomain cfcHom_continuous ContinuousMap.continuous_precomp continuous_induced_dom
eqOn_of_cfcₙ_eq_cfcₙ 📖	mathematical	cfcₙ ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Set.EqOn quasispectrum	—	ContinuousOn.restrict cfcₙHom_injective IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙ_apply
instFactMemSetQuasispectrumOfNat 📖	mathematical	—	Fact Set Set.instMembership quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	quasispectrum.zero_mem
isClosedEmbedding_cfcₙHom_of_cfcHom 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring quasispectrum.instZero IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHom_of_cfcHom ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus	—	spectrum_subset_quasispectrum continuous_inclusion Topology.IsClosedEmbedding.comp IsDomain.toNontrivial instIsDomain ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus cfcHom_isClosedEmbedding IsUniformEmbedding.isClosedEmbedding ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace CompactlyCoherentSpace.of_sequentialSpace FrechetUrysohnSpace.to_sequentialSpace Subtype.instFrechetUrysohnSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace ContinuousMap.instT0Space T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsUniformInducing.isUniformEmbedding ContinuousMapZero.instT0Space ContinuousMap.uniformSpace_eq_inf_precomp_of_cover Continuous.isProperMap ContinuousFunctionalCalculus.compactSpace_spectrum instT2SpaceSubtype ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass TopologicalSpace.NoetherianSpace.compactSpace TopologicalSpace.Finite.to_noetherianSpace Finite.of_fintype Set.range_zero Function.Injective.image_injective Subtype.val_injective Set.image_union Subtype.range_coe Set.image_singleton Set.image_univ quasispectrum_eq_spectrum_union_zero inf_uniformity Filter.comap_inf Filter.comap_comap inf_eq_left LE.le.trans le_top eq_top_iff refl_mem_uniformity ContinuousMap.ext map_zero ContinuousMapZero.instZeroHomClass Filter.comap_const_of_mem
range_cfcₙ_eq_range_cfcₙHom 📖	mathematical	—	Set.range cfcₙ SetLike.coe NonUnitalStarSubalgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgHom.range NonUnitalStarAlgHom 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMapZero.instStarRing NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass cfcₙHom	—	Set.ext IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass cfcₙ_cases ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass ContinuousOn.restrict cfcₙHom_eq_cfcₙ_extend

---

← Back to Index