image of finset in set

Stream: Is there code for X?

[Kevin Buzzard]

What's the idiomatic way to do this?

import data.finset.basic
import data.set.finite

noncomputable def finset.map_to_set (X : Type) (S : set X) (T : finset X) (hTS : (T : set X) ⊆ S) :
  finset S :=
  let setversion := {s : S | s.1 ∈ T} in
  have h : setversion.finite := sorry,
set.finite.to_finset h

[Hanting Zhang]

Is this close to something that could work?

def finset.map_to_set (X : Type) (S : set X) (T : finset X)
  [decidable_pred (λ (x : X), x ∈ S)] : finset S :=
T.subtype (∈ S)

[Hanting Zhang]

Then you could also use some of the docs#finset.subtype API

[Kevin Buzzard]

Aah this is perfect -- thanks!