Documentation Verification Report

Restrict

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

Statistics

Metric	Count
Definitions `homeomorph`, `nonUnitalStarAlgHom`, `homeomorph`, `starAlgHom`	4
Theorems `cfc`, `cfcₙHom_eq_restrict`, `cfcₙ_eq_restrict`, `continuous_nonUnitalStarAlgHom`, `isClosedEmbedding_nonUnitalStarAlgHom`, `nonUnitalClosedEmbeddingCFC`, `nonUnitalStarAlgHom_apply`, `nonUnitalStarAlgHom_id`, `nonUnitalStarAlgHom_injective`, `cfc`, `cfcHom_eq_restrict`, `cfc_eq_restrict`, `closedEmbeddingCFC`, `compactSpace`, `continuous_starAlgHom`, `isClosedEmbedding_starAlgHom`, `starAlgHom_apply`, `starAlgHom_id`, `starAlgHom_injective`	19
Total	23

QuasispectrumRestricts

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—
`nonUnitalStarAlgHom` 📖	CompOp	8 math math: `nonUnitalStarAlgHom_id`, `cfcₙHom_nnreal_eq_restrict`, `cfcₙHom_eq_restrict`, `continuous_nonUnitalStarAlgHom`, `nonUnitalStarAlgHom_injective`, `isClosedEmbedding_nonUnitalStarAlgHom`, `cfcₙHom_real_eq_restrict`, `nonUnitalStarAlgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cfc` 📖	mathematical	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike`	`NonUnitalContinuousFunctionalCalculus` `Semifield.toCommSemiring` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum` `isCompact_iff_compactSpace` `quasispectrum.preimage_algebraMap` `Topology.IsClosedEmbedding.isCompact_preimage` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `continuous_nonUnitalStarAlgHom` `cfcₙHom_continuous` `nonUnitalStarAlgHom_injective` `cfcₙHom_injective` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `nonUnitalStarAlgHom_id` `cfcₙHom_id` `nonUnitalStarAlgHom_apply` `cfcₙHom_map_quasispectrum` `Set.ext` `left_inv` `Set.mem_preimage` `quasispectrum.algebraMap_mem` `Subtype.prop` `cfcₙHom_predicate`
`cfcₙHom_eq_restrict` 📖	mathematical	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instFunLike`	`cfcₙHom` `Semifield.toCommSemiring` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `nonUnitalStarAlgHom` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Field.toSemifield` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `cfcₙHom_eq_of_continuous_of_map_id` `continuous_nonUnitalStarAlgHom` `cfcₙHom_continuous` `nonUnitalStarAlgHom_id` `cfcₙHom_id`
`cfcₙ_eq_restrict` 📖	mathematical	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike`	`cfcₙ` `Semifield.toCommSemiring` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `Field.toSemifield` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `ContinuousMap` `ContinuousMap.instFunLike`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousOn.restrict` `cfcₙ_apply` `cfcₙHom_eq_restrict` `nonUnitalStarAlgHom_apply` `cfcₙHom_eq_cfcₙ_extend` `cfcₙ_congr` `CanLift.prf` `Subtype.canLift` `Function.Injective.extend_apply` `Topology.IsEmbedding.continuousOn_iff` `Topology.IsClosedEmbedding.isEmbedding` `left_inv` `ContinuousOn.comp` `Continuous.continuousOn` `Topology.IsEmbedding.continuous` `quasispectrum.algebraMap_mem` `cfcₙ_apply_of_not_continuousOn` `cfcₙ_apply_of_not_map_zero` `map_zero` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`continuous_nonUnitalStarAlgHom` 📖	mathematical	`Continuous` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `quasispectrum.instZero` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMapZero.instTopologicalSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMapZero.instNonUnitalCommRing` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike`	`Continuous` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `quasispectrum.instZero` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMapZero.instTopologicalSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom`	—	`EuclideanDomain.toNontrivial` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.comp` `IsDomain.toNontrivial` `instIsDomain` `ContinuousMapZero.continuous_postcomp` `ContinuousMapZero.continuous_precomp`
`isClosedEmbedding_nonUnitalStarAlgHom` 📖	mathematical	`Topology.IsClosedEmbedding` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `quasispectrum.instZero` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMapZero.instTopologicalSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMapZero.instNonUnitalCommRing` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike` `IsUniformEmbedding` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Topology.IsClosedEmbedding` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `quasispectrum.instZero` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMapZero.instTopologicalSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom`	—	`EuclideanDomain.toNontrivial` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Topology.IsClosedEmbedding.comp` `IsUniformEmbedding.isClosedEmbedding` `ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `Subtype.instFrechetUrysohnSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousMapZero.instT0Space` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsUniformEmbedding.comp` `ContinuousMapZero.isUniformEmbedding_comp` `UniformEquiv.isUniformEmbedding`
`nonUnitalClosedEmbeddingCFC` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `QuasispectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`NonUnitalClosedEmbeddingContinuousFunctionalCalculus` `Semifield.toCommSemiring` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `cfc` `NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsUniformEmbedding.isClosedEmbedding` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `cfcₙHom_eq_restrict` `isClosedEmbedding_nonUnitalStarAlgHom` `cfcₙHom_isClosedEmbedding`
`nonUnitalStarAlgHom_apply` 📖	mathematical	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `quasispectrum.instZero` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom` `Field.toSemifield` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ContinuousMapZero.instNonUnitalCommRing` `ContinuousMapZero.comp` `CommSemiring.toSemiring` `StarAlgHom` `Algebra.id` `StarMul.toInvolutiveStar` `StarRing.toStarMul` `StarAlgHom.instFunLike` `StarAlgHom.ofId` `Algebra.toModule` `NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom` `Subtype.map` `ContinuousMap` `ContinuousMap.instFunLike`	—	`EuclideanDomain.toNontrivial` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `IsTopologicalSemiring.toIsSemitopologicalSemiring`
`nonUnitalStarAlgHom_id` 📖	mathematical	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instFunLike` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `quasispectrum.instZero` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMapZero.instNonUnitalCommRing` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `ContinuousMapZero.id` `instFactMemSetQuasispectrumOfNat`	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `quasispectrum.instZero` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom` `ContinuousMapZero.id` `instFactMemSetQuasispectrumOfNat`	—	`EuclideanDomain.toNontrivial` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instFactMemSetQuasispectrumOfNat` `IsDomain.toNontrivial` `instIsDomain` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.ext` `rightInvOn`
`nonUnitalStarAlgHom_injective` 📖	mathematical	`ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `quasispectrum.instZero` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMapZero.instNonUnitalCommRing` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `quasispectrum.instZero` `IsDomain.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `Module.toDistribMulAction` `ContinuousMapZero.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom`	—	`EuclideanDomain.toNontrivial` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ContinuousLinearMap.continuous` `ContinuousMapZero.postcomp_injective` `UniformEquiv.injective`

SpectrumRestricts

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—
`starAlgHom` 📖	CompOp	8 math math: `cfcHom_eq_restrict`, `isClosedEmbedding_starAlgHom`, `continuous_starAlgHom`, `cfcHom_real_eq_restrict`, `cfcHom_nnreal_eq_restrict`, `starAlgHom_apply`, `starAlgHom_id`, `starAlgHom_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cfc` 📖	mathematical	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SpectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike`	`ContinuousFunctionalCalculus` `Semifield.toCommSemiring`	—	`ContinuousFunctionalCalculus.compactSpace_spectrum` `isCompact_iff_compactSpace` `spectrum.preimage_algebraMap` `Topology.IsClosedEmbedding.isCompact_preimage` `Set.Nonempty.image` `ContinuousFunctionalCalculus.spectrum_nonempty` `image` `continuous_starAlgHom` `cfcHom_continuous` `starAlgHom_injective` `cfcHom_injective` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `starAlgHom_id` `cfcHom_id` `starAlgHom_apply` `cfcHom_map_spectrum` `Set.ext` `QuasispectrumRestricts.left_inv` `Set.mem_preimage` `spectrum.algebraMap_mem` `Subtype.prop` `cfcHom_predicate` `of_rightInvOn`
`cfcHom_eq_restrict` 📖	mathematical	`SpectrumRestricts` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instFunLike`	`cfcHom` `Semifield.toCommSemiring` `starAlgHom` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	—	`cfcHom_eq_of_continuous_of_map_id` `continuous_starAlgHom` `cfcHom_continuous` `starAlgHom_id` `cfcHom_id`
`cfc_eq_restrict` 📖	mathematical	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `SpectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike`	`cfc` `Semifield.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instFunLike`	—	`ContinuousOn.restrict` `cfc_apply` `cfcHom_eq_restrict` `starAlgHom_apply` `cfcHom_eq_cfc_extend` `cfc_congr` `CanLift.prf` `Subtype.canLift` `Function.Injective.extend_apply` `Topology.IsEmbedding.continuousOn_iff` `Topology.IsClosedEmbedding.isEmbedding` `QuasispectrumRestricts.left_inv` `ContinuousOn.comp` `Continuous.continuousOn` `Topology.IsEmbedding.continuous` `spectrum.algebraMap_mem` `cfc_apply_of_not_continuousOn`
`closedEmbeddingCFC` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SpectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`ClosedEmbeddingContinuousFunctionalCalculus` `Semifield.toCommSemiring`	—	`cfc` `ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `IsUniformEmbedding.isClosedEmbedding` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `cfcHom_eq_restrict` `isClosedEmbedding_starAlgHom` `cfcHom_isClosedEmbedding`
`compactSpace` 📖	mathematical	`SpectrumRestricts` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`CompactSpace` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`isCompact_iff_compactSpace` `IsCompact.image` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `image`
`continuous_starAlgHom` 📖	mathematical	`Continuous` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.compactOpen` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `SpectrumRestricts` `ContinuousMap.instFunLike`	`Continuous` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.compactOpen` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `starAlgHom`	—	`Continuous.comp` `ContinuousMap.continuous_postcomp` `ContinuousMap.continuous_precomp`
`isClosedEmbedding_starAlgHom` 📖	mathematical	`Topology.IsClosedEmbedding` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.compactOpen` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `SpectrumRestricts` `ContinuousMap.instFunLike` `IsUniformEmbedding` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Topology.IsClosedEmbedding` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.compactOpen` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `starAlgHom`	—	`Topology.IsClosedEmbedding.comp` `IsUniformEmbedding.isClosedEmbedding` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `Subtype.instFrechetUrysohnSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousMap.instT0Space` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsUniformEmbedding.comp` `ContinuousMap.isUniformEmbedding_comp` `UniformEquiv.isUniformEmbedding`
`starAlgHom_apply` 📖	mathematical	`SpectrumRestricts` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `starAlgHom` `ContinuousMap.comp` `CommSemiring.toSemiring` `StarMul.toInvolutiveStar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `StarRing.toStarMul` `StarAlgHom.ofId` `Subtype.map` `ContinuousMap.instFunLike`	—	—
`starAlgHom_id` 📖	mathematical	`SpectrumRestricts` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instFunLike` `StarAlgHom` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `ContinuousMap.restrict` `ContinuousMap.id`	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `starAlgHom` `ContinuousMap.restrict` `ContinuousMap.id`	—	`ContinuousMap.ext` `rightInvOn`
`starAlgHom_injective` 📖	mathematical	`ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `SpectrumRestricts` `ContinuousMap.instFunLike` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarAlgHom.instFunLike` `starAlgHom`	—	`ContinuousMap.postcomp_injective` `Homeomorph.injective`

---

← Back to Index