Documentation Verification Report

Spectrum

📁 Source: Mathlib/Analysis/Real/Spectrum.lean

Statistics

Metric	Count
Definitions	0
Theorems `le_nnreal_iff`, `lt_nnreal_iff`, `nnreal_iff`, `nnreal_of_nonneg`, `le_nnreal_iff`, `lt_nnreal_iff`, `nnreal_iff`, `nnreal_le_iff`, `nnreal_lt_iff`, `nnreal_of_nonneg`, `coe_mem_spectrum_real_of_nonneg`	11
Total	11

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_nnreal_iff` 📖	mathematical	`QuasispectrumRestricts` `NNReal` `Real` `instCommSemiringNNReal` `Real.instCommSemiring` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NNReal.instAlgebraOfReal` `CommSemiring.toSemiring` `Algebra.id` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLE` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`lt_nnreal_iff` 📖	mathematical	`QuasispectrumRestricts` `NNReal` `Real` `instCommSemiringNNReal` `Real.instCommSemiring` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NNReal.instAlgebraOfReal` `CommSemiring.toSemiring` `Algebra.id` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLT` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`nnreal_iff` 📖	mathematical	—	`QuasispectrumRestricts` `NNReal` `Real` `instCommSemiringNNReal` `Real.instCommSemiring` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NNReal.instAlgebraOfReal` `CommSemiring.toSemiring` `Algebra.id` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal` `Real.instLE` `Real.instZero`	—	`NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `quasispectrumRestricts_iff_spectrumRestricts_inr` `Unitization.quasispectrum_eq_spectrum_inr'` `SpectrumRestricts.nnreal_iff`
`nnreal_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`QuasispectrumRestricts` `NNReal` `Real` `instCommSemiringNNReal` `Real.instCommSemiring` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NNReal.instAlgebraOfReal` `CommSemiring.toSemiring` `Algebra.id` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	—	`nnreal_iff` `NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg`

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_nnreal_iff` 📖	mathematical	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLE` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`lt_nnreal_iff` 📖	mathematical	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLT` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`nnreal_iff` 📖	mathematical	—	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal` `Real.instLE` `Real.instZero`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `NNReal.coe_nonneg` `of_subset_range_algebraMap` `Real.toNNReal_coe`
`nnreal_le_iff` 📖	mathematical	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLE` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`nnreal_lt_iff` 📖	mathematical	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	`Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instLT` `NNReal.toReal`	—	`algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `Set.image_congr`
`nnreal_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SpectrumRestricts` `NNReal` `Real` `NNReal.instSemifield` `Field.toSemifield` `Real.instField` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `Real.instCommSemiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike` `ContinuousMap.realToNNReal`	—	`nnreal_iff` `spectrum_nonneg_of_nonneg`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mem_spectrum_real_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Real` `Set` `Set.instMembership` `spectrum` `Real.instCommSemiring` `NNReal.toReal` `NNReal` `instCommSemiringNNReal` `NNReal.instAlgebraOfReal` `Ring.toSemiring`	—	`SpectrumRestricts.algebraMap_image` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.left` `SpectrumRestricts.nnreal_of_nonneg` `Set.image_congr`

---

← Back to Index