∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {H K : AddSubgroup G}, H ≤ K → ∀ [H.IsFiniteRelIndex K], DiscreteTopology ↥H ↔ DiscreteTopology ↥K