Topology

📁 Source: Mathlib/RingTheory/Spectrum/Maximal/Topology.lean

Statistics

Metric	Count
Definitions zariskiTopology	1
Theorems instT1Space, toPrimeSpectrum_continuous, toPrimeSpectrum_range	3
Total	4

MaximalSpectrum

Definitions

Name	Category	Theorems
zariskiTopology 📖	CompOp	2 math math: instT1Space, toPrimeSpectrum_continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT1Space 📖	mathematical	—	T1Space MaximalSpectrum CommRing.toCommSemiring zariskiTopology	—	isClosed_induced_iff PrimeSpectrum.isClosed_singleton_iff_isMaximal isMaximal Set.preimage_image_eq toPrimeSpectrum_injective
toPrimeSpectrum_continuous 📖	mathematical	—	Continuous MaximalSpectrum CommRing.toCommSemiring PrimeSpectrum zariskiTopology PrimeSpectrum.zariskiTopology toPrimeSpectrum	—	continuous_induced_dom
toPrimeSpectrum_range 📖	mathematical	—	Set.range PrimeSpectrum CommRing.toCommSemiring MaximalSpectrum toPrimeSpectrum setOf IsClosed PrimeSpectrum.zariskiTopology Set Set.instSingletonSet	—	Set.ext isMaximal

---

← Back to Index