ProCGroups/InverseSystems.lean
1import ProCGroups.InverseSystems.CategoryBridge
2import ProCGroups.InverseSystems.CountableModels
3import ProCGroups.InverseSystems.Exactness
4import ProCGroups.InverseSystems.FiniteStageFactorization
5import ProCGroups.InverseSystems.ProfiniteLimits
6import ProCGroups.InverseSystems.Quotients
7import ProCGroups.InverseSystems.StagewiseIso
9/-
10PUBLIC_PAGE_SNAPSHOT
11generated_at: 2026-05-27T09:47:29+09:00
12lean_source: lean4/ProCGroups/InverseSystems.lean
13translation_root: data/translation
14purpose: identifies the local data snapshot used to build pages/
15placement: after imports, never before imports
16-/
17/-!
18# Inverse systems and inverse limits
20Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
21-/