subset of a subtype

Stream: general

[Scott Morrison]

Does anyone know if this is already in the library?

/-- A subset of a subtype can be thought of as a subset of the type. -/
def set_of_subtype_set {α : Type*} {P : α → Prop} (x : set {a : α // P a}) : set α :=
{a : α | ∃ (h : P a), (⟨a,h⟩ : {a : α // P a}) ∈ x}

[Sebastien Gouezel]

Isn't it just subtype.val '' x?

[Chris Hughes]

subtype.val '' x is what I write when I want that thing. Not the most obvious way of thinking about it.

[Chris Hughes]

But it is automatically a subgroup or whatever else you might want.

[Scott Morrison]

Thank you! :-) :embarrassed: