Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC