Documentation Verification Report

Hom

📁 Source: Mathlib/Topology/Spectral/Hom.lean

Statistics

Metric	Count
Definitions `IsSpectralMap`, `SpectralMap`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `toContinuousMap`, `toFun`, `SpectralMapClass`, `instCoeTCSpectralMapOfSpectralMapClass`	11
Theorems `preimage_of_isOpen`, `isSpectralMap`, `comp`, `continuous`, `isCompact_preimage_of_isOpen`, `toContinuous`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_continuousMap`, `coe_comp_continuousMap'`, `coe_copy`, `coe_id`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instSpectralMapClass`, `spectral'`, `toFun_eq_coe`, `map_spectral`, `toContinuousMapClass`, `isSpectralMap_id`	27
Total	38

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_of_isOpen` 📖	mathematical	`IsSpectralMap` `IsCompact` `IsOpen`	`Set.preimage`	—	`IsSpectralMap.isCompact_preimage_of_isOpen`

IsProperMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSpectralMap` 📖	mathematical	`IsProperMap`	`IsSpectralMap`	—	`toContinuous` `isCompact_preimage`

IsSpectralMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`IsSpectralMap`	—	—	`Continuous.comp` `continuous` `IsCompact.preimage_of_isOpen` `IsOpen.preimage`
`continuous` 📖	mathematical	`IsSpectralMap`	`Continuous`	—	`toContinuous`
`isCompact_preimage_of_isOpen` 📖	mathematical	`IsSpectralMap` `IsOpen` `IsCompact`	`Set.preimage`	—	—
`toContinuous` 📖	mathematical	`IsSpectralMap`	`Continuous`	—	—

SpectralMap

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	8 math math: `cancel_left`, `coe_comp_continuousMap'`, `coe_comp`, `id_comp`, `cancel_right`, `comp_assoc`, `comp_apply`, `comp_id`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	4 math math: `id_comp`, `coe_id`, `comp_id`, `id_apply`
`instFunLike` 📖	CompOp	9 math math: `coe_comp_continuousMap'`, `coe_comp`, `ext_iff`, `coe_comp_continuousMap`, `toFun_eq_coe`, `comp_apply`, `coe_id`, `id_apply`, `instSpectralMapClass`
`instInhabited` 📖	CompOp	—
`toContinuousMap` 📖	CompOp	—
`toFun` 📖	CompOp	2 math math: `spectral'`, `toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `SpectralMap` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `SpectralMap` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff` `of_eq` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike` `comp`	—	—
`coe_comp_continuousMap` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `SpectralMapClass.toContinuousMapClass` `instSpectralMapClass`	—	—
`coe_comp_continuousMap'` 📖	mathematical	—	`toContinuousMap` `SpectralMap` `instFunLike` `SpectralMapClass.toContinuousMapClass` `instSpectralMapClass` `comp` `ContinuousMap.comp`	—	`SpectralMapClass.toContinuousMapClass` `instSpectralMapClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `SpectralMap` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike` `id`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `SpectralMap` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `SpectralMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `SpectralMap` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instSpectralMapClass` 📖	mathematical	—	`SpectralMapClass` `SpectralMap` `instFunLike`	—	`spectral'`
`spectral'` 📖	mathematical	—	`IsSpectralMap` `toFun`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `SpectralMap` `instFunLike`	—	—

SpectralMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_spectral` 📖	mathematical	—	`IsSpectralMap` `DFunLike.coe`	—	—
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass`	—	`IsSpectralMap.continuous` `map_spectral`

(root)

Definitions

Name	Category	Theorems
`IsSpectralMap` 📖	CompData	8 math math: `SpectralMap.spectral'`, `IsRetrocompact_iff_isSpectralMap_subtypeVal`, `AlgebraicGeometry.Scheme.Hom.isSpectralMap`, `SpectralMapClass.map_spectral`, `IsProperMap.isSpectralMap`, `isSpectralMap_id`, `AlgebraicGeometry.quasiCompact_iff_spectral`, `AlgebraicGeometry.quasiCompact_iff_isSpectralMap`
`SpectralMap` 📖	CompData	9 math math: `SpectralMap.coe_comp_continuousMap'`, `SpectralMap.coe_comp`, `SpectralMap.ext_iff`, `SpectralMap.coe_comp_continuousMap`, `SpectralMap.toFun_eq_coe`, `SpectralMap.comp_apply`, `SpectralMap.coe_id`, `SpectralMap.id_apply`, `SpectralMap.instSpectralMapClass`
`SpectralMapClass` 📖	CompData	1 math math: `SpectralMap.instSpectralMapClass`
`instCoeTCSpectralMapOfSpectralMapClass` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSpectralMap_id` 📖	mathematical	—	`IsSpectralMap`	—	`continuous_id`

---

← Back to Index