Documentation Verification Report

Topology

📁 Source: FLT/Deformations/Algebra/InverseLimit/Topology.lean

Statistics

Metric	Count
Definitions `instTopologicalSpace`	1
Theorems `instIsTopologicalGroup`, `instIsTopologicalModule`, `instIsTopologicalRing`, `lift_continuous`, `toComponent_continuous`, `val_continuous`	6
Total	7

InverseLimit

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	6 math math: `lift_continuous`, `instIsTopologicalGroup`, `instIsTopologicalModule`, `instIsTopologicalRing`, `val_continuous`, `toComponent_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalGroup` 📖	mathematical	—	`InverseLimit` `instTopologicalSpace` `instGroup`	—	—
`instIsTopologicalModule` 📖	mathematical	`IsTopologicalModule`	`InverseLimit` `instAddCommGroupOfAddMonoidHomClass` `instModule` `instTopologicalSpace`	—	`Submodule.instIsTopologicalModuleSubtypeMem` `Pi.instTopologicalModule`
`instIsTopologicalRing` 📖	mathematical	—	`InverseLimit` `instTopologicalSpace` `instRingOfRingHomClass`	—	—
`lift_continuous` 📖	mathematical	`InverseSystemHom`	`InverseLimit` `instTopologicalSpace` `lift`	—	`lift_def`
`toComponent_continuous` 📖	mathematical	—	`InverseLimit` `instTopologicalSpace` `toComponent`	—	`toComponent_def` `val_continuous`
`val_continuous` 📖	mathematical	—	`InverseLimit` `instTopologicalSpace`	—	—

---

← Back to Index