Prop-valued substructure

Stream: new members

[Philippe Duchon]

Say I have some type G and a Group G. Does Mathlib provide a Prop-valued way of saying "this subset of G is actually a subgroup"? Or should one simply build a Subgroup G structure?

(I would like to have a theorem statement of the form, "under such and such assumption on a subset A, this Ais actually a subgroup", with the statement mentioning A; if I just build a subgroup structure, I might as well be building a trivial subgroup unrelated to A)

[Kyle Miller]

One way to express it:

example {G : Type _} [Group G] (A : Set G) :
    ∃ H : Subgroup G, A = H := sorry

[Kyle Miller]

A more indirect way:

example {G : Type _} [Group G] (A : Set G) :
    Subgroup.closure A = A := sorry