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`, `isClosedEmbedding_nonUnitalStarAlgHom`, `nonUnitalStarAlgHom_apply`, `nonUnitalStarAlgHom_id`, `cfc`, `cfcHom_eq_restrict`, `cfc_eq_restrict`, `compactSpace`, `isClosedEmbedding_starAlgHom`, `starAlgHom_apply`, `starAlgHom_id`	13
Total	17

QuasispectrumRestricts

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cfc` 📖	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`	`NonUnitalContinuousFunctionalCalculus` `IsDomain.toNontrivial` `instIsDomain`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum` `isCompact_iff_compactSpace` `quasispectrum.preimage_algebraMap` `Topology.IsClosedEmbedding.isCompact_preimage` `IsUniformEmbedding.isClosedEmbedding` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `isClosedEmbedding_nonUnitalStarAlgHom` `cfcₙHom_isClosedEmbedding` `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	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `QuasispectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`cfcₙHom` `IsDomain.toNontrivial` `instIsDomain` `nonUnitalStarAlgHom` `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` `Topology.IsClosedEmbedding.continuous` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `isClosedEmbedding_nonUnitalStarAlgHom` `cfcₙHom_isClosedEmbedding` `nonUnitalStarAlgHom_id` `cfcₙHom_id`
`cfcₙ_eq_restrict` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `QuasispectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`cfcₙ` `IsDomain.toNontrivial` `instIsDomain` `EuclideanDomain.toNontrivial` `Field.toEuclideanDomain` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing`	—	`EuclideanDomain.toNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `IsDomain.toNontrivial` `instIsDomain` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `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` `IsUniformEmbedding.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`
`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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SMulCommClass.continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `QuasispectrumRestricts` `ContinuousMap` `ContinuousMap.instFunLike` `IsUniformEmbedding` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`IsDomain.toNontrivial` `instIsDomain` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `nonUnitalStarAlgHom`	—	`EuclideanDomain.toNontrivial` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `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`
`nonUnitalStarAlgHom_apply` 📖	mathematical	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `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` `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` `CommSemiring.toSemiring` `Algebra.id` `IsTopologicalSemiring.toContinuousMul` `Semiring.toNonUnitalSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `nonUnitalStarAlgHom` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ContinuousMapZero.instNonUnitalCommRing` `ContinuousMapZero.comp` `StarAlgHom` `StarMul.toInvolutiveStar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `StarRing.toStarMul` `StarAlgHom.instFunLike` `StarAlgHom.ofId` `Algebra.toModule` `NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom` `Subtype.map`	—	`EuclideanDomain.toNontrivial` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `IsDomain.toNontrivial` `instIsDomain`
`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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `Semiring.toModule` `SMulCommClass.continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalStarAlgHom.instFunLike` `ContinuousMapZero.id` `instFactMemSetQuasispectrumOfNat`	`IsDomain.toNontrivial` `instIsDomain` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `ContinuousMapZero.instNonUnitalCommSemiring` `nonUnitalStarAlgHom`	—	`EuclideanDomain.toNontrivial` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `instFactMemSetQuasispectrumOfNat` `IsDomain.toNontrivial` `instIsDomain` `ContinuousMapZero.ext` `rightInvOn`

SpectrumRestricts

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cfc` 📖	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`	`ContinuousFunctionalCalculus`	—	`ContinuousFunctionalCalculus.compactSpace_spectrum` `isCompact_iff_compactSpace` `spectrum.preimage_algebraMap` `Topology.IsClosedEmbedding.isCompact_preimage` `IsUniformEmbedding.isClosedEmbedding` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `Set.Nonempty.image` `ContinuousFunctionalCalculus.spectrum_nonempty` `image` `isClosedEmbedding_starAlgHom` `cfcHom_isClosedEmbedding` `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	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `SpectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`cfcHom` `starAlgHom`	—	`cfcHom_eq_of_continuous_of_map_id` `Topology.IsClosedEmbedding.continuous` `isClosedEmbedding_starAlgHom` `cfcHom_isClosedEmbedding` `starAlgHom_id` `cfcHom_id`
`cfc_eq_restrict` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `SpectrumRestricts` `ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.instFunLike`	`cfc`	—	`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` `IsUniformEmbedding.isEmbedding` `QuasispectrumRestricts.left_inv` `ContinuousOn.comp` `Continuous.continuousOn` `Topology.IsEmbedding.continuous` `spectrum.algebraMap_mem` `cfc_apply_of_not_continuousOn`
`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`
`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`	`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`	`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` `starAlgHom` `ContinuousMap.comp` `CommSemiring.toSemiring` `StarMul.toInvolutiveStar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `StarRing.toStarMul` `StarAlgHom.ofId` `Subtype.map`	—	—
`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`	`starAlgHom`	—	`ContinuousMap.ext` `rightInvOn`

---

← Back to Index