Documentation Verification Report

Topology

📁 Source: Mathlib/Data/Analysis/Topology.lean

Statistics

Metric	Count
Definitions `Realizer`, `Ctop`, `Realizer`, `F`, `id`, `nhds`, `ofEquiv`, `σ`, `f`, `instCoeFunForallSet`, `inter`, `ofEquiv`, `toRealizer`, `toTopsp`, `top`, `Realizer`, `bas`, `sets`, `instInhabitedCtopSet`, `instInhabitedRealizer`, `instInhabitedRealizerEmptyCollectionSet`	21
Theorems `eq`, `ext`, `ext'`, `isClosed_iff`, `isOpen`, `isOpen_iff`, `is_basis`, `mem_interior_iff`, `mem_nhds`, `nhds_F`, `nhds_σ`, `ofEquiv_F`, `ofEquiv_σ`, `tendsto_nhds_iff`, `coe_mk`, `inter_mem`, `inter_sub`, `mem_nhds_toTopsp`, `ofEquiv_val`, `toTopsp_isTopologicalBasis`, `top_mem`, `to_locallyFinite`, `instNonemptyRealizerOfFinite`, `locallyFinite_iff_exists_realizer`	24
Total	45

Compact

Definitions

Name	Category	Theorems
`Realizer` 📖	CompOp	—

Ctop

Definitions

Name	Category	Theorems
`Realizer` 📖	CompData	—
`f` 📖	CompOp	14 math math: `mem_nhds_toTopsp`, `coe_mk`, `Realizer.nhds_σ`, `Realizer.is_basis`, `Realizer.nhds_F`, `top_mem`, `Realizer.mem_interior_iff`, `Realizer.mem_nhds`, `Realizer.isOpen_iff`, `toTopsp_isTopologicalBasis`, `ofEquiv_val`, `Realizer.ofEquiv_F`, `Realizer.tendsto_nhds_iff`, `Realizer.isOpen`
`instCoeFunForallSet` 📖	CompOp	—
`inter` 📖	CompOp	2 math math: `inter_mem`, `inter_sub`
`ofEquiv` 📖	CompOp	1 math math: `ofEquiv_val`
`toRealizer` 📖	CompOp	—
`toTopsp` 📖	CompOp	5 math math: `mem_nhds_toTopsp`, `Realizer.ext`, `Realizer.ext'`, `toTopsp_isTopologicalBasis`, `Realizer.eq`
`top` 📖	CompOp	1 math math: `top_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`Set` `Set.instMembership` `Set.instHasSubset` `Set.instInter`	`f`	—	—
`inter_mem` 📖	mathematical	`Set` `Set.instMembership` `Set.instInter` `f`	`inter`	—	—
`inter_sub` 📖	mathematical	`Set` `Set.instMembership` `Set.instInter` `f`	`Set.instHasSubset` `inter`	—	—
`mem_nhds_toTopsp` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `toTopsp` `Set.instMembership` `f` `Set.instHasSubset`	—	`TopologicalSpace.IsTopologicalBasis.mem_nhds_iff` `toTopsp_isTopologicalBasis`
`ofEquiv_val` 📖	mathematical	—	`f` `ofEquiv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`toTopsp_isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `toTopsp` `Set.range` `Set` `f`	—	`inter_mem` `inter_sub` `Set.eq_univ_iff_forall` `top_mem`
`top_mem` 📖	mathematical	—	`Set` `Set.instMembership` `f` `top`	—	—

Ctop.Realizer

Definitions

Name	Category	Theorems
`F` 📖	CompOp	10 math math: `nhds_σ`, `is_basis`, `nhds_F`, `mem_interior_iff`, `mem_nhds`, `isOpen_iff`, `ofEquiv_F`, `eq`, `tendsto_nhds_iff`, `isOpen`
`id` 📖	CompOp	—
`nhds` 📖	CompOp	2 math math: `nhds_σ`, `nhds_F`
`ofEquiv` 📖	CompOp	2 math math: `ofEquiv_σ`, `ofEquiv_F`
`σ` 📖	CompOp	11 math math: `nhds_σ`, `is_basis`, `nhds_F`, `ofEquiv_σ`, `mem_interior_iff`, `mem_nhds`, `isOpen_iff`, `ofEquiv_F`, `eq`, `tendsto_nhds_iff`, `isOpen`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`Ctop.toTopsp` `σ` `F`	—	—
`ext` 📖	mathematical	`IsOpen` `Ctop.f` `Set` `Set.instMembership` `Set.instHasSubset`	`Ctop.toTopsp`	—	`ext'` `mem_nhds_iff`
`ext'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `Ctop.f` `Set.instHasSubset`	`Ctop.toTopsp`	—	`TopologicalSpace.ext_nhds` `Filter.ext` `Ctop.mem_nhds_toTopsp`
`isClosed_iff` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	`isOpen_compl_iff` `isOpen_iff` `not_imp_comm`
`isOpen` 📖	mathematical	—	`IsOpen` `Ctop.f` `σ` `F`	—	`isOpen_iff_nhds` `mem_nhds` `Set.Subset.refl`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `Set` `Set.instMembership` `Ctop.f` `σ` `F` `Set.instHasSubset`	—	`isOpen_iff_mem_nhds` `mem_nhds`
`is_basis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Set.range` `Set` `σ` `Ctop.f` `F`	—	`Ctop.toTopsp_isTopologicalBasis` `eq`
`mem_interior_iff` 📖	mathematical	—	`Set` `Set.instMembership` `interior` `Ctop.f` `σ` `F` `Set.instHasSubset`	—	`mem_interior_iff_mem_nhds` `mem_nhds`
`mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `Ctop.f` `σ` `F` `Set.instHasSubset`	—	`Ctop.mem_nhds_toTopsp` `eq`
`nhds_F` 📖	mathematical	—	`CFilter.f` `Set` `Filter.Realizer.σ` `nhds` `nhds` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.Realizer.F` `Ctop.f` `σ` `F` `Set.instMembership`	—	—
`nhds_σ` 📖	mathematical	—	`Filter.Realizer.σ` `nhds` `nhds` `σ` `Set` `Set.instMembership` `Ctop.f` `F`	—	—
`ofEquiv_F` 📖	mathematical	—	`Ctop.f` `σ` `ofEquiv` `F` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Ctop.ofEquiv_val`
`ofEquiv_σ` 📖	mathematical	—	`σ` `ofEquiv`	—	—
`tendsto_nhds_iff` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Set` `Set.instMembership` `Ctop.f` `σ` `F`	—	`Filter.Realizer.tendsto_iff`

LocallyFinite

Definitions

Name	Category	Theorems
`Realizer` 📖	CompData	2 math math: `locallyFinite_iff_exists_realizer`, `instNonemptyRealizerOfFinite`

LocallyFinite.Realizer

Definitions

Name	Category	Theorems
`bas` 📖	CompOp	—
`sets` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_locallyFinite` 📖	mathematical	—	`LocallyFinite`	—	`Ctop.Realizer.mem_nhds` `Set.Subset.rfl` `Set.toFinite` `Finite.of_fintype`

(root)

Definitions

Name	Category	Theorems
`Ctop` 📖	CompData	—
`instInhabitedCtopSet` 📖	CompOp	—
`instInhabitedRealizer` 📖	CompOp	—
`instInhabitedRealizerEmptyCollectionSet` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonemptyRealizerOfFinite` 📖	mathematical	—	`LocallyFinite.Realizer`	—	`locallyFinite_iff_exists_realizer` `locallyFinite_of_finite`
`locallyFinite_iff_exists_realizer` 📖	mathematical	—	`LocallyFinite` `LocallyFinite.Realizer`	—	`Classical.axiom_of_choice` `Ctop.Realizer.mem_nhds` `Set.Finite.subset` `Set.Nonempty.mono` `Set.inter_subset_inter_right` `LocallyFinite.Realizer.to_locallyFinite`

---

← Back to Index