Nikolov–Segal strong completeness theorem | Lean AI formalization leaderboard

Problem statement

Notes: Every finite-index subgroup of a topologically finitely generated profinite group is open.

Source: Nikolay Nikolov and Dan Segal, *On finitely generated profinite groups, I: strong completeness and uniform bounds*, Annals of Mathematics 165 (2007), no. 1, 171–238, Theorem 1.1, https://doi.org/10.4007/annals.2007.165.171; *On finitely generated profinite groups, II: products in quasisimple groups*, Annals of Mathematics 165 (2007), no. 1, 239–273, https://doi.org/10.4007/annals.2007.165.239.

Informal solution: See Nikolov and Segal, Parts I and II, cited in `source`.

theorem declaration uses `sorry`nikolov_segal (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : LeanEval.GroupTheory.IsTopologicallyFinitelyGenerated G)
    (H : Subgroup G) [H.FiniteIndex] :
    IsOpen (H : Set G) := byG:Type u_1inst✝⁵:Group Ginst✝⁴:TopologicalSpace Ginst✝³:IsTopologicalGroup Ginst✝²:CompactSpace Ginst✝¹:TotallyDisconnectedSpace GhG:IsTopologicallyFinitelyGenerated GH:Subgroup Ginst✝:H.FiniteIndex⊢ IsOpen ↑H
  sorryAll goals completed! 🐙