ClassFieldTower.ProP.exists_eq_top_of_monotone_closedSubgroups
A dense increasing union of closed subgroups of a finitely generated pro-p group reaches the whole group at a finite stage.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
open ProCGroups.Generation ProCGroups.FiniteGeneration
universe uLean source · statement
theorem exists_eq_top_of_monotone_closedSubgroups
{p : ℕ} [Fact p.Prime]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hpro : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
(hfg : TopologicallyFinitelyGenerated G)
(H : ℕ → Subgroup G) (hmono : Monotone H)
(hclosed : ∀ n, IsClosed (H n : Set G))
(hdense : (⨆ n, H n).topologicalClosure = ⊤) :
∃ n, H n = ⊤