Stream: Is there code for X?

Topic: Membership-Proof in filter

Marcus Rossel (Dec 28 2020 at 16:58):

I need to filter over a finset, and within the filter-predicate I need a proof that the current element is a member of the set over which I'm filtering. So in something like:

import data.finset

def aaa (t : finset ℕ) (n : { x // x ∈ t }) : Prop := sorry

def bbb (s : finset ℕ) : finset ℕ := s.filter (λ m, aaa s m)


... I would either want m to have type { y // y ∈ s }, or get some proof of m ∈ s.
Is there code for this?

Bhavik Mehta (Dec 28 2020 at 17:13):

docs#finset.attach

Last updated: May 07 2021 at 22:14 UTC