src/ZF/Perm.thy
changeset 9570 e16e168984e1
parent 2469 b50b8c0eec01
child 13176 312bd350579b
equal deleted inserted replaced
9569:68400ff46b09 9570:e16e168984e1
     7   -- Composition of relations, the identity relation
     7   -- Composition of relations, the identity relation
     8   -- Injections, surjections, bijections
     8   -- Injections, surjections, bijections
     9   -- Lemmas for the Schroeder-Bernstein Theorem
     9   -- Lemmas for the Schroeder-Bernstein Theorem
    10 *)
    10 *)
    11 
    11 
    12 Perm = upair + mono + func +
    12 Perm = mono + func +
    13 consts
    13 consts
    14   O     :: [i,i]=>i      (infixr 60)
    14   O     :: [i,i]=>i      (infixr 60)
    15 
    15 
    16 defs
    16 defs
    17   (*composition of relations and functions; NOT Suppes's relative product*)
    17   (*composition of relations and functions; NOT Suppes's relative product*)