ssreflect - [ssreflect] Bijection between subsets

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Bijection between subsets

From: Florent Hivert <>
To: "" <>
Subject: [ssreflect] Bijection between subsets
Date: Thu, 21 Apr 2016 10:46:49 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:wfhHtBaBiKuLXETzAZQ++Vz/LSx+4OfEezUN459isYplN5qZpcS5bnLW6fgltlLVR4KTs6sC0LqG9f6wEjRfqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7D0pc2YO1oArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Ku4jVqZVAjArOHwd4dbx8BjFVwqGoHoaSGQf1BRSSUCR9wrgU5n1vyDmnu9mwmybO9f3RPY1Xy6j5uFlUkm7pj0AMmsX9GbNh8psxIJavh+7u1Qr7YrTeoyTKLxef73QZ88yQXBAGMhLAX8SSrigZpcCWrJSdd1TqJPw8gMD

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

[ssreflect] Bijection between subsets, Florent Hivert, 04/21/2016
- RE: [ssreflect] Bijection between subsets, Georges Gonthier, 04/21/2016
  - [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
    - Re: [ssreflect] ListSet in ssreflect, Laurent Thery, 04/21/2016
      - Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Laurent Thery, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
    - Re: [ssreflect] ListSet in ssreflect, Cyril, 04/21/2016
      - Re: [ssreflect] ListSet in ssreflect, Christian Doczkal, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016

List archive

[ssreflect] Bijection between subsets