Documentation Verification Report

Section2

📁 Source: Hochster/Section2.lean

Statistics

Metric	Count
Definitions `ConstructibleTop`, `instTopologicalSpace`, `ofConstructibleTop`, `toConstructibleTop`, `isClosedSubbasis`	5
Theorems `instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`, `instT2SpaceOfT0SpaceOfCompactSpaceOfQuasiSeparatedSpaceOfPrespectralSpace`, `instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`, `instTopologicalSpace_eq_induced_of_isEmbedding_isSpectralMap`, `instTopologicalSpace_le`, `isClosedSubbasis_isClosed_union_isOpen_isCompact`, `inter_sInter_nonempty_of_isCompact_isClosed_mem`, `biInter_mem_of_finiteInter`, `of_le_of_isClosed`, `of_le_of_isCompact`, `continuous_constructibleTop`, `isClosed_range`, `of_continuous_of_continuous_constructibleTop`, `biInter_mem_of_finiteInter`, `sInter_mem_of_finiteInter`, `sInter_ne_empty_of_finiteInter_finiteInter_of_subset_union`, `generateFrom_booleanSubalgebra_closure`, `generateFrom_booleanSubalgebra_closure_eq_of_isSublattice`, `generateFrom_isConstructible_eq_generateFrom_union_compl_image`, `generateFrom_latticeClosure`, `isClosedSubbasis_iff_isTopologicalBasis_sInter_compl`, `subbasis_iff_isTopologicalBasis_sInter`, `sInter_isIrreducible_of_isClosed_mem`, `sInter_ne_empty_of_isClosed_mem`, `compactSpace_of_isEmbedding_of_isClosed_constructibleTop_range`, `exist_isClosed_union_isClosed_of_isClosed_not_isPreirreducible`, `exist_open_disjoint_or_mem_pt_closure`, `exists_of_isOpen_isCompact_isEmbedding`, `finiteInter_isOpen_and_isCompact`, `isOpen_and_isCompact_iff_exists_of_isEmbedding_of_isClosed_constructibleTop_range`, `isSpectralMap_iff_continuous_and_continuous_constructibleTop`, `mem_patch_closure_iff_mem_pt_closure`, `prespectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range`, `quasiSeparatedSpace_of_isEmbedding_of_isClosed_constructibleTop_range`, `quasiSober_of_isEmbedding_of_isClosed_constructibleTop_range`, `singleton_closure_inter_open_nonempty_iff`, `spectralSpace_and_isSpectralMap_iff_isClosed_constructibleTop_range`, `spectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range`	38
Total	43

ConstructibleTop

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	14 math math: `IsSpectralMap.isClosed_range`, `instTopologicalSpace_eq_induced_of_isEmbedding_isSpectralMap`, `SpringLike'.vanishing_set_is_patch_of_mem_closure_insert_div`, `isClosedSubbasis_isClosed_union_isOpen_isCompact`, `instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`, `SpringLike'.support_is_patch_of_mem_closure_insert_div`, `spectralSpace_and_isSpectralMap_iff_isClosed_constructibleTop_range`, `instT2SpaceOfT0SpaceOfCompactSpaceOfQuasiSeparatedSpaceOfPrespectralSpace`, `instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`, `IsSpectralMap.continuous_constructibleTop`, `isSpectralMap_iff_continuous_and_continuous_constructibleTop`, `instTopologicalSpace_le`, `PrimeSpectrum.ConstructibleTop.isTopologicalBasis_inter_biInter`, `SpringCat.range_isClosed`
`ofConstructibleTop` 📖	CompOp	—
`toConstructibleTop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` 📖	mathematical	—	`ConstructibleTop` `instTopologicalSpace`	—	`instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `Ultrafilter.sInter_isIrreducible_of_isClosed_mem` `singleton_closure_inter_open_nonempty_iff` `Filter.inter_sInter_nonempty_of_isCompact_isClosed_mem`
`instT2SpaceOfT0SpaceOfCompactSpaceOfQuasiSeparatedSpaceOfPrespectralSpace` 📖	mathematical	—	`ConstructibleTop` `instTopologicalSpace`	—	`instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`
`instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` 📖	mathematical	—	`instTopologicalSpace`	—	`instTopologicalSpace.eq_1` `TopologicalSpace.generateFrom_isConstructible_eq_generateFrom_union_compl_image`
`instTopologicalSpace_eq_induced_of_isEmbedding_isSpectralMap` 📖	mathematical	—	`instTopologicalSpace`	—	`instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `instTopologicalSpace_le` `TopologicalSpace.generateFrom_isConstructible_eq_generateFrom_union_compl_image` `exists_of_isOpen_isCompact_isEmbedding`
`instTopologicalSpace_le` 📖	mathematical	—	`ConstructibleTop` `instTopologicalSpace`	—	`instTopologicalSpace.eq_1` `TopologicalSpace.generateFrom_isConstructible_eq_generateFrom_union_compl_image`
`isClosedSubbasis_isClosed_union_isOpen_isCompact` 📖	mathematical	—	`TopologicalSpace.isClosedSubbasis` `ConstructibleTop` `instTopologicalSpace`	—	`instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_sInter_nonempty_of_isCompact_isClosed_mem` 📖	—	—	—	—	—

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_mem_of_finiteInter` 📖	—	—	—	—	`Set.Finite.biInter_mem_of_finiteInter`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_le_of_isClosed` 📖	—	—	—	—	—

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_le_of_isCompact` 📖	—	—	—	—	—

IsSpectralMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_constructibleTop` 📖	mathematical	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	`ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`
`isClosed_range` 📖	mathematical	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	`ConstructibleTop.instT2SpaceOfT0SpaceOfCompactSpaceOfQuasiSeparatedSpaceOfPrespectralSpace` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` `continuous_constructibleTop`
`of_continuous_of_continuous_constructibleTop` 📖	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	—	`ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` `ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `IsCompact.of_le_of_isCompact` `ConstructibleTop.instTopologicalSpace_le`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_mem_of_finiteInter` 📖	—	—	—	—	`sInter_mem_of_finiteInter`
`sInter_mem_of_finiteInter` 📖	—	—	—	—	—
`sInter_ne_empty_of_finiteInter_finiteInter_of_subset_union` 📖	—	—	—	—	`sInter_mem_of_finiteInter`

TopologicalSpace

Definitions

Name	Category	Theorems
`isClosedSubbasis` 📖	MathDef	2 math math: `isClosedSubbasis_iff_isTopologicalBasis_sInter_compl`, `ConstructibleTop.isClosedSubbasis_isClosed_union_isOpen_isCompact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generateFrom_booleanSubalgebra_closure` 📖	—	—	—	—	`generateFrom_latticeClosure` `generateFrom_booleanSubalgebra_closure_eq_of_isSublattice`
`generateFrom_booleanSubalgebra_closure_eq_of_isSublattice` 📖	—	—	—	—	—
`generateFrom_isConstructible_eq_generateFrom_union_compl_image` 📖	—	—	—	—	`generateFrom_booleanSubalgebra_closure`
`generateFrom_latticeClosure` 📖	—	—	—	—	—
`isClosedSubbasis_iff_isTopologicalBasis_sInter_compl` 📖	mathematical	—	`isClosedSubbasis`	—	`subbasis_iff_isTopologicalBasis_sInter`
`subbasis_iff_isTopologicalBasis_sInter` 📖	—	—	—	—	—

Ultrafilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sInter_isIrreducible_of_isClosed_mem` 📖	—	—	—	—	`sInter_ne_empty_of_isClosed_mem` `exist_isClosed_union_isClosed_of_isClosed_not_isPreirreducible` `Filter.inter_sInter_nonempty_of_isCompact_isClosed_mem`
`sInter_ne_empty_of_isClosed_mem` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`ConstructibleTop` 📖	CompOp	12 math math: `IsSpectralMap.isClosed_range`, `SpringLike'.vanishing_set_is_patch_of_mem_closure_insert_div`, `ConstructibleTop.isClosedSubbasis_isClosed_union_isOpen_isCompact`, `SpringLike'.support_is_patch_of_mem_closure_insert_div`, `spectralSpace_and_isSpectralMap_iff_isClosed_constructibleTop_range`, `ConstructibleTop.instT2SpaceOfT0SpaceOfCompactSpaceOfQuasiSeparatedSpaceOfPrespectralSpace`, `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`, `IsSpectralMap.continuous_constructibleTop`, `isSpectralMap_iff_continuous_and_continuous_constructibleTop`, `ConstructibleTop.instTopologicalSpace_le`, `PrimeSpectrum.ConstructibleTop.isTopologicalBasis_inter_biInter`, `SpringCat.range_isClosed`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`IsCompact.of_le_of_isCompact` `ConstructibleTop.instTopologicalSpace_le` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`
`exist_isClosed_union_isClosed_of_isClosed_not_isPreirreducible` 📖	—	—	—	—	—
`exist_open_disjoint_or_mem_pt_closure` 📖	—	—	—	—	`ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` `Set.Finite.sInter_ne_empty_of_finiteInter_finiteInter_of_subset_union`
`exists_of_isOpen_isCompact_isEmbedding` 📖	—	—	—	—	—
`finiteInter_isOpen_and_isCompact` 📖	—	—	—	—	—
`isOpen_and_isCompact_iff_exists_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`exists_of_isOpen_isCompact_isEmbedding` `ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `IsCompact.of_le_of_isCompact` `ConstructibleTop.instTopologicalSpace_le` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`
`isSpectralMap_iff_continuous_and_continuous_constructibleTop` 📖	mathematical	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	`IsSpectralMap.continuous_constructibleTop` `IsSpectralMap.of_continuous_of_continuous_constructibleTop`
`mem_patch_closure_iff_mem_pt_closure` 📖	—	—	—	—	`ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` `Set.Finite.sInter_mem_of_finiteInter`
`prespectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`isOpen_and_isCompact_iff_exists_of_isEmbedding_of_isClosed_constructibleTop_range`
`quasiSeparatedSpace_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`isOpen_and_isCompact_iff_exists_of_isEmbedding_of_isClosed_constructibleTop_range`
`quasiSober_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace` `IsClosed.of_le_of_isClosed` `ConstructibleTop.instTopologicalSpace_le` `ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`
`singleton_closure_inter_open_nonempty_iff` 📖	—	—	—	—	—
`spectralSpace_and_isSpectralMap_iff_isClosed_constructibleTop_range` 📖	mathematical	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	`IsSpectralMap.isClosed_range` `spectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range` `ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image` `IsCompact.of_le_of_isCompact` `ConstructibleTop.instTopologicalSpace_le` `ConstructibleTop.instCompactSpaceOfQuasiSoberOfQuasiSeparatedSpaceOfPrespectralSpace`
`spectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range` 📖	—	—	—	—	`compactSpace_of_isEmbedding_of_isClosed_constructibleTop_range` `quasiSober_of_isEmbedding_of_isClosed_constructibleTop_range` `quasiSeparatedSpace_of_isEmbedding_of_isClosed_constructibleTop_range` `prespectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range`

---

← Back to Index