All.lean
Nyll.SchemeTheory.Topology.All
0 declarations indexed from sourceView source ↗
Module documentation
Topological results used by scheme theory.
Imports34
- Nyll.SchemeTheory.Topology.ConstantSheafDiscreteFunctions
- Nyll.SchemeTheory.Topology.SpecializationCofinalSections
- Nyll.SchemeTheory.Topology.SheafPullbackStalks
- Nyll.SchemeTheory.Topology.ConnectedComponents
- Nyll.SchemeTheory.Topology.ConnectedComponentsMap
- Nyll.SchemeTheory.Topology.ConnectedComponentsSeparation
- Nyll.SchemeTheory.Topology.SpectralClosedRestriction
- Nyll.SchemeTheory.Topology.FiniteSkyscraperEmbedding
- Nyll.SchemeTheory.Topology.ClosedConstantSkyscraper
- Nyll.SchemeTheory.Topology.FiniteCoverFilteredColimit
- Nyll.SchemeTheory.Topology.CompactOpenGenerators
- Nyll.SchemeTheory.Topology.CompactOpenSections
- Nyll.SchemeTheory.Topology.CompactOpenPresentable
- Nyll.SchemeTheory.Topology.CompactOpenFiniteModels
- Nyll.SchemeTheory.Topology.FiniteModelSheafTransitions
- Nyll.SchemeTheory.Topology.FiniteModelPrincipalStalk
- Nyll.SchemeTheory.Topology.SheafPullbackGerms
- Nyll.SchemeTheory.Topology.SpecializationCofinalRestriction
- Nyll.SchemeTheory.Topology.FiniteModelSheafDiagram
- Nyll.SchemeTheory.Topology.FiniteModelStalkColimit
- Nyll.SchemeTheory.Topology.SheafApproximationGerms
- Nyll.SchemeTheory.Topology.FiniteModelStalkComparison
- Nyll.SchemeTheory.Topology.FiniteModelSheafColimit
- Nyll.SchemeTheory.Topology.FilteredColimitRestriction
- Nyll.SchemeTheory.Topology.ClosedDiscreteSheaf
- Nyll.SchemeTheory.Topology.ClosedDiscreteRestriction
- Nyll.SchemeTheory.Topology.ClosedDiscreteStalkOutside
- Nyll.SchemeTheory.Topology.SpectralClosedSubspaceRestriction
- Nyll.SchemeTheory.Topology.ClosedDiscreteRestrictionMono
- Nyll.SchemeTheory.Topology.SpectralClosedDiscreteRestriction
- Nyll.SchemeTheory.Topology.PullbackFiniteSkyscraperEmbedding
- Nyll.SchemeTheory.Topology.PullbackSkyscraperClosedDiscrete
- Nyll.SchemeTheory.Topology.FiniteProductRestriction
- Nyll.SchemeTheory.Topology.SpectralClosedSheafRestriction
Imported by1
This module has no indexed declarations. Its imports and full source are available here.