{G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      (carrier : Set G) →
        (∀ {a b : G}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier) →
          1 ∈ carrier → (∀ {x : G}, x ∈ carrier → x⁻¹ ∈ carrier) → IsOpen carrier → OpenSubgroup G