Documentation Verification Report

Prespectral

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

Statistics

Metric	Count
Definitions `PrespectralSpace`, `opensEquiv`	2
Theorems `exists_opens_image_eq_of_prespectralSpace`, `exists_isCompact_and_isOpen_between`, `isBasis_opens`, `isTopologicalBasis`, `of_isClosedEmbedding`, `of_isInducing`, `of_isOpenCover`, `of_isTopologicalBasis`, `of_isTopologicalBasis'`, `sigma`, `prespectralSpace`, `instLocallyCompactSpaceOfPrespectralSpace`, `instPrespectralSpaceOfNoetherianSpace`, `instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace`, `prespectralSpace_iff`	15
Total	17

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_opens_image_eq_of_prespectralSpace` 📖	mathematical	`Continuous` `IsOpenMap` `Set` `Set.instHasSubset` `Set.range` `IsOpen` `IsCompact`	`TopologicalSpace.Opens.carrier` `Set.image` `SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike`	—	`IsOpen.preimage` `TopologicalSpace.Opens.isBasis_iff_cover` `PrespectralSpace.isBasis_opens` `IsCompact.elim_finite_subcover` `TopologicalSpace.Opens.is_open'` `TopologicalSpace.Opens.mem_sSup` `Set.mem_iUnion` `isOpen_iUnion` `Set.iUnion_congr_Prop` `Set.Finite.isCompact_biUnion` `Finset.finite_toSet` `Set.iUnion_coe_set` `Set.image_iUnion` `subset_antisymm` `Set.instAntisymmSubset`

PrespectralSpace

Definitions

Name	Category	Theorems
`opensEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isCompact_and_isOpen_between` 📖	—	`IsCompact` `IsOpen` `Set` `Set.instHasSubset`	—	—	`IsCompact.induction_on` `Set.instReflSubset` `subset_trans` `Set.instIsTransSubset` `IsCompact.union` `IsOpen.union` `Set.union_subset_union` `Set.union_subset` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `isTopologicalBasis` `mem_nhdsWithin` `Set.inter_subset_left` `subset_rfl`
`isBasis_opens` 📖	mathematical	—	`TopologicalSpace.Opens.IsBasis` `setOf` `TopologicalSpace.Opens` `IsCompact` `SetLike.coe` `TopologicalSpace.Opens.instSetLike`	—	`Set.ext` `TopologicalSpace.Opens.is_open'` `isTopologicalBasis`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `setOf` `Set` `IsOpen` `IsCompact`	—	—
`of_isClosedEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding`	`PrespectralSpace`	—	`of_isInducing` `Topology.IsClosedEmbedding.isInducing` `IsProperMap.isSpectralMap` `Topology.IsClosedEmbedding.isProperMap`
`of_isInducing` 📖	mathematical	`Topology.IsInducing` `IsSpectralMap`	`PrespectralSpace`	—	`of_isTopologicalBasis` `TopologicalSpace.IsTopologicalBasis.isInducing` `isTopologicalBasis` `IsSpectralMap.isCompact_preimage_of_isOpen`
`of_isOpenCover` 📖	—	`TopologicalSpace.IsOpenCover` `PrespectralSpace` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	—	—	`of_isTopologicalBasis` `TopologicalSpace.IsOpenCover.isTopologicalBasis` `isTopologicalBasis` `IsCompact.image` `continuous_subtype_val`
`of_isTopologicalBasis` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `IsCompact`	`PrespectralSpace`	—	`TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset` `TopologicalSpace.IsTopologicalBasis.isOpen`
`of_isTopologicalBasis'` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `Set.range` `Set` `IsCompact`	`PrespectralSpace`	—	`of_isTopologicalBasis`
`sigma` 📖	mathematical	`PrespectralSpace`	`instTopologicalSpaceSigma`	—	`of_isTopologicalBasis` `TopologicalSpace.IsTopologicalBasis.sigma` `isTopologicalBasis` `IsCompact.image` `continuous_sigmaMk`

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prespectralSpace` 📖	mathematical	`Topology.IsOpenEmbedding`	`PrespectralSpace`	—	`TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds` `TopologicalSpace.IsTopologicalBasis.isOpen_iff` `PrespectralSpace.isTopologicalBasis` `isOpen_iff_image_isOpen` `IsOpen.preimage` `continuous` `Topology.IsInducing.isCompact_preimage'` `Topology.IsEmbedding.toIsInducing` `toIsEmbedding` `Set.SurjOn.subset_range` `Function.Injective.mem_set_image` `Topology.IsEmbedding.injective`

(root)

Definitions

Name	Category	Theorems
`PrespectralSpace` 📖	CompData	10 math math: `AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat`, `PrespectralSpace.of_isTopologicalBasis`, `PrespectralSpace.of_isTopologicalBasis'`, `SpectralSpace.toPrespectralSpace`, `PrimeSpectrum.instPrespectralSpace`, `prespectralSpace_iff`, `PrespectralSpace.of_isClosedEmbedding`, `Topology.IsOpenEmbedding.prespectralSpace`, `instPrespectralSpaceOfNoetherianSpace`, `PrespectralSpace.of_isInducing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallyCompactSpaceOfPrespectralSpace` 📖	mathematical	—	`LocallyCompactSpace`	—	`TopologicalSpace.IsTopologicalBasis.mem_nhds_iff` `PrespectralSpace.isTopologicalBasis` `IsOpen.mem_nhds`
`instPrespectralSpaceOfNoetherianSpace` 📖	mathematical	—	`PrespectralSpace`	—	`PrespectralSpace.of_isTopologicalBasis` `TopologicalSpace.isTopologicalBasis_opens` `TopologicalSpace.NoetherianSpace.isCompact`
`instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace` 📖	mathematical	—	`TotallySeparatedSpace`	—	`totallySeparatedSpace_iff_exists_isClopen` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `PrespectralSpace.isTopologicalBasis` `IsClosed.isOpen_compl` `isClosed_singleton` `T2Space.t1Space` `IsCompact.isClosed`
`prespectralSpace_iff` 📖	mathematical	—	`PrespectralSpace` `TopologicalSpace.IsTopologicalBasis` `setOf` `Set` `IsOpen` `IsCompact`	—	—

---

← Back to Index