Compactness.lean

theorem maximal_open_normal_intersections_compactness_step
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (K : Subgroup G) [K.Normal] (hKclosed : IsClosed (K : Set G))
    (𝓜 : Set (Subgroup G))
    (hMclosed : ∀ M ∈ 𝓜, IsClosed (M : Set G))
    (hfinite :
      ∀ S : Set (Subgroup G), S.Finite → S ⊆ 𝓜 → sInf S ⊔ K = ⊤) :
    sInf 𝓜 ⊔ K = ⊤

theorem maximal_open_normal_intersections_nonabelian_simple
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (K : Subgroup G) [K.Normal] [IsSimpleGroup (G ⧸ K)]
    (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
    (hKclosed : IsClosed (K : Set G))
    (𝓜 : Set (Subgroup G))
    (hMnormal : ∀ M ∈ 𝓜, M.Normal)
    (hMclosed : ∀ M ∈ 𝓜, IsClosed (M : Set G))
    (hMtop : ∀ M ∈ 𝓜, M ⊔ K = ⊤) :
    sInf 𝓜 ⊔ K = ⊤