Hi, suppose I have a finite sequence of n disjoint sets, given by a function (f :num -> ‘a -> bool), and their union is BIGUNION (IMAGE f (count n)), and an order R (antisymmetric , transitive) on these sets.
Is it possible to assert the existence of another function (g :num -> ‘a ->
bool) such that:
BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))
and
!i j. i < n /\ j < n ==> R (g i) (g j)
?
That’s, I want to “sort” these set according to this order. Does it exist for
sure? Is there anything from the existing “sortingTheory” that I can leverage?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
