Basic

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

Statistics

Metric	Count
Definitions SpectralSpace	1
Theorems toCompactSpace, toPrespectralSpace, toQuasiSeparatedSpace, toQuasiSober, toT0Space, spectralSpace	6
Total	7

SpectralSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompactSpace 📖	mathematical	—	CompactSpace	—	—
toPrespectralSpace 📖	mathematical	—	PrespectralSpace	—	—
toQuasiSeparatedSpace 📖	mathematical	—	QuasiSeparatedSpace	—	—
toQuasiSober 📖	mathematical	—	QuasiSober	—	—
toT0Space 📖	mathematical	—	T0Space	—	—

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectralSpace 📖	mathematical	Topology.IsOpenEmbedding	SpectralSpace	—	quasiSober SpectralSpace.toQuasiSober prespectralSpace SpectralSpace.toPrespectralSpace quasiSeparatedSpace SpectralSpace.toQuasiSeparatedSpace Topology.IsEmbedding.t0Space SpectralSpace.toT0Space isEmbedding

(root)

Definitions

Name	Category	Theorems
SpectralSpace 📖	CompData	2 math math: Topology.IsOpenEmbedding.spectralSpace, PrimeSpectrum.instSpectralSpace

---

← Back to Index