Documentation Verification Report

ConstructibleTopology

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

Statistics

Metric	Count
Definitions `WithConstructibleTopology`, `constructibleTopology`, `constructibleTopologySubbasis`, `instTopologicalSpaceWithConstructibleTopology`	4
Theorems `isOpen_constructibleTopology_of_isClosed`, `isOpen_constructibleTopology_of_isOpen`, `compactSpace_withConstructibleTopology`, `compl_mem_constructibleTopologySubbasis_iff`, `isCompact_of_mem_constructibleTopologySubbasis`, `isCompact_sInter_of_subset_constructibleTopologySubbasis`	6
Total	10

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_constructibleTopology_of_isClosed` 📖	mathematical	`IsCompact` `Compl.compl` `Set` `Set.instCompl`	`IsOpen` `constructibleTopology`	—	`TopologicalSpace.isOpen_generateFrom_of_mem`
`isOpen_constructibleTopology_of_isOpen` 📖	mathematical	`IsCompact` `IsOpen`	`IsOpen` `constructibleTopology`	—	`TopologicalSpace.isOpen_generateFrom_of_mem`

(root)

Definitions

Name	Category	Theorems
`WithConstructibleTopology` 📖	CompOp	1 math math: `compactSpace_withConstructibleTopology`
`constructibleTopology` 📖	CompOp	2 math math: `IsCompact.isOpen_constructibleTopology_of_isOpen`, `IsCompact.isOpen_constructibleTopology_of_isClosed`
`constructibleTopologySubbasis` 📖	CompOp	1 math math: `compl_mem_constructibleTopologySubbasis_iff`
`instTopologicalSpaceWithConstructibleTopology` 📖	CompOp	1 math math: `compactSpace_withConstructibleTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_withConstructibleTopology` 📖	mathematical	—	`CompactSpace` `WithConstructibleTopology` `instTopologicalSpaceWithConstructibleTopology`	—	`compactSpace_generateFrom_of_compl_mem` `zorn_subset_nonempty` `DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_sUnion_of_subset` `subset_rfl` `isClosed_sInter` `CompactSpace.nonempty_sInter` `Maximal.prop` `subset_trans` `Set.instIsTransSubset` `IsIrreducible.isGenericPoint_genericPoint` `Set.mem_sInter` `Set.sInter_subset_of_mem` `IsGenericPoint.mem` `IsGenericPoint.mem_open_set_iff` `Set.inter_comm` `IsCompact.nonempty_inter_sInter` `Set.sInter_insert` `PrespectralSpace.exists_isClosed_of_not_isPreirreducible` `Set.not_nonempty_iff_eq_empty` `isCompact_sInter_of_subset_constructibleTopologySubbasis` `Set.Finite.union` `Set.Finite.diff` `Set.sInter_union` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq`
`compl_mem_constructibleTopologySubbasis_iff` 📖	mathematical	—	`Set` `Set.instMembership` `constructibleTopologySubbasis` `Compl.compl` `Set.instCompl`	—	—
`isCompact_of_mem_constructibleTopologySubbasis` 📖	mathematical	`Set` `Set.instMembership` `constructibleTopologySubbasis`	`IsCompact`	—	`IsClosed.isCompact`
`isCompact_sInter_of_subset_constructibleTopologySubbasis` 📖	mathematical	`Set` `Set.instHasSubset` `constructibleTopologySubbasis`	`IsCompact` `Set.sInter`	—	`QuasiSeparatedSpace.isCompact_sInter` `isCompact_of_mem_constructibleTopologySubbasis`

---

← Back to Index