Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hello Florent,
This wouldn't be a valid specification, because it says nothing about f 
mapping s to t. A minimal correct specification would be {in s &, injective 
f} /\ f @: s = t, from which you could derive both bijective properties if 
you need them. Do note the {on t, bijective f} property is mostly used as a 
precondition for  the reindex lemma for bigops, and that you can just as 
easily use reindex_inj or big_imset in this case.
   Best,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Florent Hivert
Sent: 21 April 2016 09:47
To: 

Subject: [ssreflect] Bijection between subsets

      Hi there,

I'm not sure how to properly use {in ...} and {on ...} constructions.
I'm given to finite set s t : {set T} and I'd like to assert that I'm able to 
construct a bijection between those two sets. Is the following statement the 
right way to go:

  exists f : T -> T, {in s, bijective f} /\ {on t, bijective f}.

cheers,

Florent