Continuity

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

Statistics

Metric	Count
Definitions	0
Theorems cfc, cfc', cfc_fun, cfc_nnreal, cfc_nnreal', cfc_nnreal_of_mem_nhdsSet, cfc_of_mem_nhdsSet, cfcₙ, cfcₙ', cfcₙ_fun, cfcₙ_nnreal, cfcₙ_nnreal', cfcₙ_nnreal_of_mem_nhdsSet, cfcₙ_of_mem_nhdsSet, cfc, cfc_nnreal, cfcₙ, cfcₙ_nnreal, cfc, cfc', cfc_fun, cfc_nnreal, cfc_nnreal', cfc_nnreal_of_mem_nhdsSet, cfc_of_mem_nhdsSet, cfcₙ, cfcₙ', cfcₙ_fun, cfcₙ_nnreal, cfcₙ_nnreal', cfcₙ_nnreal_of_mem_nhdsSet, cfcₙ_of_mem_nhdsSet, cfc, cfc_nnreal, cfcₙ, cfcₙ_nnreal, cfc, cfc_nnreal, cfcₙ, cfcₙ_nnreal, continuousAt_cfc_fun, continuousAt_cfcₙ_fun, continuousOn_cfc, continuousOn_cfc_nnreal, continuousOn_cfc_nnreal_setProd, continuousOn_cfc_setProd, continuousOn_cfcₙ, continuousOn_cfcₙ_nnreal, continuousOn_cfcₙ_nnreal_setProd, continuousOn_cfcₙ_setProd, continuousWithinAt_cfc_fun, continuousWithinAt_cfcₙ_fun, continuous_cfcHomSuperset_left, continuous_cfcₙHomSuperset_left, lipschitzOnWith_cfc_fun, lipschitzOnWith_cfc_fun_of_subset, lipschitzOnWith_cfcₙ_fun, lipschitzOnWith_cfcₙ_fun_of_subset, tendsto_cfc_fun, tendsto_cfcₙ_fun	60
Total	60

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsCompact SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Eventually Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra nhds	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc nhdsWithin_univ
cfc' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Continuous NormedRing.toSeminormedRing Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc'
cfc_fun 📖	mathematical	Continuous UniformOnFun Set Set.instSingletonSet spectrum UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun	cfc	—	continuousOn_univ ContinuousOn.cfc_fun
cfc_nnreal 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsCompact NNReal NNReal.instTopologicalSpace Filter.Eventually Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField nhds	cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc_nnreal nhdsWithin_univ
cfc_nnreal' 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField ContinuousOn	cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc_nnreal'
cfc_nnreal_of_mem_nhdsSet 📖	mathematical	Set NNReal Filter Filter.instMembership nhdsSet NNReal.instTopologicalSpace Set.iUnion spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ContinuousOn	cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc_nnreal_of_mem_nhdsSet Set.iUnion_congr_Prop Set.iUnion_true
cfc_of_mem_nhdsSet 📖	mathematical	Set Filter Filter.instMembership nhdsSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.iUnion spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Continuous ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfc_of_mem_nhdsSet Set.iUnion_congr_Prop Set.iUnion_true
cfcₙ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing IsCompact SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Eventually Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ nhdsWithin_univ
cfcₙ' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Continuous NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ'
cfcₙ_fun 📖	mathematical	Continuous UniformOnFun Set Set.instSingletonSet quasispectrum UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun	cfcₙ	—	continuousOn_univ ContinuousOn.cfcₙ_fun
cfcₙ_nnreal 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing IsCompact NNReal NNReal.instTopologicalSpace Filter.Eventually Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup nhds instZeroNNReal	cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ_nnreal nhdsWithin_univ
cfcₙ_nnreal' 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup ContinuousOn instZeroNNReal	cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ_nnreal'
cfcₙ_nnreal_of_mem_nhdsSet 📖	mathematical	Set NNReal Filter Filter.instMembership nhdsSet NNReal.instTopologicalSpace Set.iUnion quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace ContinuousOn instZeroNNReal	cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet Set.iUnion_congr_Prop Set.iUnion_true
cfcₙ_of_mem_nhdsSet 📖	mathematical	Set Filter Filter.instMembership nhdsSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.iUnion quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Continuous NonUnitalSeminormedRing.toPseudoMetricSpace ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_univ ContinuousOn.cfcₙ_of_mem_nhdsSet Set.iUnion_congr_Prop Set.iUnion_true

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousAt NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra nhds ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.Tendsto.cfc tendsto Filter.Eventually.self_of_nhds
cfc_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField nhds Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousOn	cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.Tendsto.cfc_nnreal tendsto Filter.Eventually.self_of_nhds
cfcₙ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousAt NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup nhds ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.Tendsto.cfcₙ tendsto Filter.Eventually.self_of_nhds
cfcₙ_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup nhds Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ContinuousOn instZeroNNReal	cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.Tendsto.cfcₙ_nnreal tendsto Filter.Eventually.self_of_nhds

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra nhdsWithin	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus eq_1 ContinuousWithinAt.cfc Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfc' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn NormedRing.toSeminormedRing Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfc Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfc_fun 📖	mathematical	ContinuousOn UniformOnFun Set Set.instSingletonSet spectrum UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun	cfc	—	eq_1 continuousWithinAt_cfc_fun Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfc_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField nhdsWithin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus eq_1 ContinuousWithinAt.cfc_nnreal Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfc_nnreal' 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfc_nnreal Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfc_nnreal_of_mem_nhdsSet 📖	mathematical	Set NNReal Filter Filter.instMembership nhdsSet NNReal.instTopologicalSpace Set.iUnion Set.instMembership spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_isCompact locallyCompact_of_proper NNReal.instProperSpace spectrum.isCompact_nnreal spectrum.instCompactSpace instProperSpaceReal nhdsSet_iUnion Filter.Eventually.mono UpperHemicontinuous.upperHemicontinuousAt upperHemicontinuous_spectrum_nnreal subset_of_mem_nhdsSet cfc_nnreal Filter.Tendsto.eventually continuousWithinAt mono
cfc_of_mem_nhdsSet 📖	mathematical	Set Filter Filter.instMembership nhdsSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.iUnion Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_isCompact locallyCompact_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real spectrum.isCompact nhdsSet_iUnion Filter.Eventually.mono UpperHemicontinuous.upperHemicontinuousAt upperHemicontinuous_spectrum subset_of_mem_nhdsSet cfc Filter.Tendsto.eventually continuousWithinAt mono
cfcₙ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus eq_1 ContinuousWithinAt.cfcₙ Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfcₙ' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfcₙ_fun 📖	mathematical	ContinuousOn UniformOnFun Set Set.instSingletonSet quasispectrum UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun UniformSpace.toTopologicalSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfcₙ	—	eq_1 continuousWithinAt_cfcₙ_fun Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfcₙ_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup nhdsWithin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instZeroNNReal	cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus eq_1 ContinuousWithinAt.cfcₙ_nnreal Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfcₙ_nnreal' 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instZeroNNReal	cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_nnreal Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem'
cfcₙ_nnreal_of_mem_nhdsSet 📖	mathematical	Set NNReal Filter Filter.instMembership nhdsSet NNReal.instTopologicalSpace Set.iUnion Set.instMembership quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace instZeroNNReal	cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_isCompact locallyCompact_of_proper NNReal.instProperSpace quasispectrum.isCompact_nnreal quasispectrum.instCompactSpace instProperSpaceReal nhdsSet_iUnion Filter.Eventually.mono UpperHemicontinuous.upperHemicontinuousAt upperHemicontinuous_quasispectrum_nnreal subset_of_mem_nhdsSet cfcₙ_nnreal Filter.Tendsto.eventually continuousWithinAt mono
cfcₙ_of_mem_nhdsSet 📖	mathematical	Set Filter Filter.instMembership nhdsSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.iUnion Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing ContinuousOn NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_isCompact locallyCompact_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real quasispectrum.isCompact nhdsSet_iUnion Filter.Eventually.mono UpperHemicontinuous.upperHemicontinuousAt upperHemicontinuous_quasispectrum subset_of_mem_nhdsSet cfcₙ Filter.Tendsto.eventually continuousWithinAt mono

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set Set.instMembership ContinuousWithinAt NormedRing.toSeminormedRing Filter.Eventually Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra nhdsWithin ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.Tendsto.cfc tendsto Filter.Eventually.self_of_nhdsWithin
cfc_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Set Set.instMembership ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Filter.Eventually Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField nhdsWithin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousOn	cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.Tendsto.cfc_nnreal tendsto Filter.Eventually.self_of_nhdsWithin
cfcₙ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set Set.instMembership ContinuousWithinAt NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup nhdsWithin ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Filter.Tendsto.cfcₙ tendsto Filter.Eventually.self_of_nhdsWithin
cfcₙ_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Set Set.instMembership ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup nhdsWithin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ContinuousOn instZeroNNReal	cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Filter.Tendsto.cfcₙ_nnreal tendsto Filter.Eventually.self_of_nhdsWithin

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Tendsto nhds NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra ContinuousOn	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar comp IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus ContinuousWithinAt.tendsto ContinuousOn.continuousWithinAt continuousOn_cfc tendsto_nhdsWithin_iff Filter.Eventually.and
cfc_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Filter.Eventually Set Set.instHasSubset spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousOn	cfc instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal comp NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus ContinuousWithinAt.tendsto ContinuousOn.continuousWithinAt continuousOn_cfc_nnreal tendsto_nhdsWithin_iff Filter.Eventually.and
cfcₙ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Tendsto nhds NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar comp NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus ContinuousWithinAt.tendsto ContinuousOn.continuousWithinAt continuousOn_cfcₙ tendsto_nhdsWithin_iff Filter.Eventually.and
cfcₙ_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Filter.Eventually Set Set.instHasSubset quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ContinuousOn instZeroNNReal	cfcₙ instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal comp NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus ContinuousWithinAt.tendsto ContinuousOn.continuousWithinAt continuousOn_cfcₙ_nnreal tendsto_nhdsWithin_iff Filter.Eventually.and

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_cfc_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace nhds spectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace	ContinuousAt cfc	—	tendsto_cfc_fun
continuousAt_cfcₙ_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace nhds quasispectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	ContinuousAt cfcₙ	—	tendsto_cfcₙ_fun
continuousOn_cfc 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn	NormedRing.toSeminormedRing cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace setOf Set Set.instHasSubset spectrum	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_iff_continuous_restrict ContinuousOn.restrict cfcHomSuperset_apply Set.restrict_apply ContinuousOn.mono cfc_apply ContinuousMap.continuous_toFun continuous_cfcHomSuperset_left continuous_subtype_val
continuousOn_cfc_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace setOf Set Set.instHasSubset spectrum	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus cfc_nnreal_eq_real ContinuousOn.congr ContinuousOn.ofReal_map_toNNReal Set.mapsTo_image_iff Real.toNNReal_coe ContinuousOn.mono IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar continuousOn_cfc IsCompact.image NNReal.continuous_coe SpectrumRestricts.eq_1 IsScalarTower.right Algebra.to_smulCommClass NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Real.instNontrivial IsometricContinuousFunctionalCalculus.toNonUnital SpectrumRestricts.algebraMap_image NNReal.instIsScalarTowerOfReal IsScalarTower.left Set.image_mono
continuousOn_cfc_nnreal_setProd 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace	ContinuousOn UniformOnFun Set Set.instSingletonSet instTopologicalSpaceProd UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal UniformSpace.toTopologicalSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing cfc Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun SProd.sprod Set.instSProd setOf Set.instHasSubset spectrum	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal continuousOn_prod_of_continuousOn_lipschitzOnWith Finite.of_fintype NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_cfc_nnreal lipschitzOnWith_cfc_fun_of_subset Nonneg.instIsometricContinuousFunctionalCalculus
continuousOn_cfc_setProd 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	ContinuousOn UniformOnFun Set Set.instSingletonSet instTopologicalSpaceProd UniformOnFun.topologicalSpace NormedRing.toSeminormedRing cfc Semifield.toCommSemiring Field.toSemifield NormedField.toField RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NormedRing.toRing NormedAlgebra.toAlgebra IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun SProd.sprod Set.instSProd setOf Set.instHasSubset spectrum	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar continuousOn_prod_of_continuousOn_lipschitzOnWith Finite.of_fintype IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus continuousOn_cfc lipschitzOnWith_cfc_fun_of_subset
continuousOn_cfcₙ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace setOf Set Set.instHasSubset quasispectrum	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_iff_continuous_restrict quasispectrum.zero_mem IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousOn.restrict cfcₙHomSuperset_apply Set.restrict_apply ContinuousOn.mono cfcₙ_apply ContinuousMap.continuous_toFun ContinuousMapZero.map_zero' continuous_cfcₙHomSuperset_left continuous_subtype_val Set.eq_empty_iff_forall_notMem continuousOn_empty
continuousOn_cfcₙ_nnreal 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace ContinuousOn instZeroNNReal	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace setOf Set Set.instHasSubset quasispectrum	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus cfcₙ_nnreal_eq_real ContinuousOn.congr ContinuousOn.ofReal_map_toNNReal Set.mapsTo_image_iff Real.toNNReal_coe ContinuousOn.mono IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar continuousOn_cfcₙ IsCompact.image NNReal.continuous_coe Real.toNNReal_zero QuasispectrumRestricts.algebraMap_image IsScalarTower.left Set.image_mono
continuousOn_cfcₙ_nnreal_setProd 📖	mathematical	IsCompact NNReal NNReal.instTopologicalSpace	ContinuousOn UniformOnFun Set Set.instSingletonSet instTopologicalSpaceProd UniformOnFun.topologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal UniformSpace.toTopologicalSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing instCommSemiringNNReal instNontrivialNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun SProd.sprod Set.instSProd setOf instZeroNNReal Set.instHasSubset quasispectrum	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal continuousOn_prod_of_continuousOn_lipschitzOnWith Finite.of_fintype NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_cfcₙ_nnreal lipschitzOnWith_cfcₙ_fun_of_subset Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus
continuousOn_cfcₙ_setProd 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	ContinuousOn UniformOnFun Set Set.instSingletonSet instTopologicalSpaceProd UniformOnFun.topologicalSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun SProd.sprod Set.instSProd setOf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Set.instHasSubset quasispectrum	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar continuousOn_prod_of_continuousOn_lipschitzOnWith Finite.of_fintype NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_cfcₙ lipschitzOnWith_cfcₙ_fun_of_subset
continuousWithinAt_cfc_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace nhdsWithin spectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace	ContinuousWithinAt cfc	—	tendsto_cfc_fun
continuousWithinAt_cfcₙ_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace nhdsWithin quasispectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	ContinuousWithinAt cfcₙ	—	tendsto_cfcₙ_fun
continuous_cfcHomSuperset_left 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Continuous NormedRing.toSeminormedRing Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra	DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set.instMembership MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid RCLike.toStarRing RCLike.instContinuousStar Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHomSuperset IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus NormedRing.toMetricSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar isCompact_iff_compactSpace ContinuousMap.induction_on_of_compact IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus AlgHomClass.commutes StarAlgHom.instAlgHomClass continuous_const cfcHomSuperset_id StarHomClass.map_star StarAlgHom.instStarHomClass Continuous.star IsTopologicalSemiring.toContinuousAdd map_add SemilinearMapClass.toAddHomClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Continuous.add NonUnitalSeminormedRing.toIsTopologicalRing map_mul NonUnitalAlgSemiHomClass.toMulHomClass Continuous.mul continuous_of_uniform_approx_of_continuous Filter.HasBasis.forall_iff Metric.uniformity_basis_dist_le dist_eq_norm Filter.frequently_iff Metric.closedBall_mem_nhds SeminormedAddCommGroup.toIsTopologicalAddGroup map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass cfcHomSuperset_apply ContinuousFunctionalCalculus.compactSpace_spectrum Isometry.norm_map_of_map_zero isometry_cfcHom map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass ContinuousMap.norm_le LT.lt.le dist_comm
continuous_cfcₙHomSuperset_left 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Continuous NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup	DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem Set.zeroOfFactMem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set.instMembership quasispectrum.zero_mem IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing instTopologicalSpaceSubtype MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule SMulCommClass.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid ContinuousMapZero.instStarRing RCLike.toStarRing RCLike.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike cfcₙHomSuperset NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus NonUnitalNormedRing.toMetricSpace	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar isCompact_iff_compactSpace ContinuousMapZero.induction_on_of_compact quasispectrum.zero_mem IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass continuous_const cfcₙHomSuperset_id StarHomClass.map_star NonUnitalStarAlgHom.instStarHomClass Continuous.star map_add SemilinearMapClass.toAddHomClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalAlgHomClass.instLinearMapClass Continuous.add NonUnitalSeminormedRing.toIsTopologicalRing map_mul NonUnitalAlgSemiHomClass.toMulHomClass Continuous.mul map_smul SemilinearMapClass.toMulActionSemiHomClass Continuous.const_smul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul continuous_of_uniform_approx_of_continuous Filter.HasBasis.forall_iff Metric.uniformity_basis_dist_le dist_eq_norm Filter.frequently_iff Metric.closedBall_mem_nhds map_sub cfcₙHomSuperset_apply NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum Isometry.norm_map_of_map_zero isometry_cfcₙHom ContinuousMapZero.instContinuousMapClass ContinuousMapZero.norm_def ContinuousMap.norm_le LT.lt.le dist_comm
lipschitzOnWith_cfc_fun 📖	mathematical	—	LipschitzOnWith UniformOnFun Set Set.instSingletonSet spectrum UniformOnFun.instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Finite.of_fintype Set.Elem Set.fintypeSingleton NNReal instOneNNReal cfc UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun setOf ContinuousOn	—	Finite.of_fintype IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus ContinuousOn.restrict cfc_apply ContinuousFunctionalCalculus.compactSpace_spectrum Isometry.edist_eq isometry_cfcHom one_mul UniformOnFun.edist_continuousRestrict_of_singleton le_refl cfc_apply_of_not_predicate LipschitzWith.lipschitzOnWith LipschitzWith.const'
lipschitzOnWith_cfc_fun_of_subset 📖	mathematical	Set Set.instHasSubset spectrum	LipschitzOnWith UniformOnFun Set.instSingletonSet UniformOnFun.instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Finite.of_fintype Set.Elem Set.fintypeSingleton NNReal instOneNNReal cfc UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun setOf ContinuousOn	—	Finite.of_fintype IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus lipschitzOnWith_cfc_fun UniformOnFun.lipschitzWith_one_ofFun_toFun' Set.sUnion_singleton LipschitzWith.lipschitzOnWith mul_one LipschitzOnWith.comp ContinuousOn.mono
lipschitzOnWith_cfcₙ_fun 📖	mathematical	—	LipschitzOnWith UniformOnFun Set Set.instSingletonSet quasispectrum UniformOnFun.instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Finite.of_fintype Set.Elem Set.fintypeSingleton NNReal instOneNNReal cfcₙ UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun setOf ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finite.of_fintype NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousOn.restrict cfcₙ_apply NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum Isometry.edist_eq isometry_cfcₙHom one_mul ContinuousMapZero.isometry_toContinuousMap UniformOnFun.edist_continuousRestrict_of_singleton le_refl cfcₙ_apply_of_not_predicate LipschitzWith.lipschitzOnWith LipschitzWith.const'
lipschitzOnWith_cfcₙ_fun_of_subset 📖	mathematical	Set Set.instHasSubset quasispectrum	LipschitzOnWith UniformOnFun Set.instSingletonSet UniformOnFun.instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Finite.of_fintype Set.Elem Set.fintypeSingleton NNReal instOneNNReal cfcₙ UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun setOf ContinuousOn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finite.of_fintype UniformOnFun.lipschitzWith_one_ofFun_toFun' Set.sUnion_singleton LipschitzWith.lipschitzOnWith NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus mul_one LipschitzOnWith.comp lipschitzOnWith_cfcₙ_fun ContinuousOn.mono
tendsto_cfc_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace	Filter.Tendsto cfc nhds	—	Filter.eq_or_neBot TendstoUniformlyOn.continuousOn Filter.Eventually.frequently Filter.tendsto_comap'_iff Subtype.range_coe_subtype ContinuousOn.restrict cfc_apply Filter.Tendsto.comp Continuous.tendsto cfcHom_continuous ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn ContinuousFunctionalCalculus.compactSpace_spectrum cfc_apply_of_not_predicate tendsto_const_nhds
tendsto_cfcₙ_fun 📖	mathematical	TendstoUniformlyOn PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	Filter.Tendsto cfcₙ nhds	—	Filter.eq_or_neBot TendstoUniformlyOn.continuousOn Filter.Eventually.frequently tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.Tendsto.congr' Filter.EventuallyEq.symm tendsto_const_nhds TendstoUniformlyOn.tendsto_at quasispectrum.zero_mem Filter.Eventually.and Filter.tendsto_comap'_iff Subtype.range_coe_subtype IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousOn.restrict cfcₙ_apply Filter.Tendsto.comp Continuous.tendsto cfcₙHom_continuous ContinuousMapZero.instContinuousMapClass Topology.IsInducing.tendsto_nhds_iff Topology.IsEmbedding.isInducing ContinuousMapZero.isEmbedding_toContinuousMap ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum cfcₙ_apply_of_not_predicate

---

← Back to Index