Nuprl Definition : leaders-finite

Finitely many leaders ==

leaders:Id List
((

b:

. (leader b

leaders))

(

l

leaders.

b:

. (l = (leader b))))

Definitions : list: type List, and: P

Q, all:

x:A. B[x], l_member: (x

l), l_all: (

x

L.P[x]), exists:

x:A. B[x], nat:

, equal: s = t, Id: Id, apply: f a
FDL editor aliases : leaders-finite

Finitely many leaders == \mexists{}leaders:Id List. ((\mforall{}b:\mBbbN{}. (leader b \mmember{} leaders)) \mwedge{} (\mforall{}l\mmember{}leaders.\mexists{}b:\mBbbN{}. (l = (leader b)))) Date html generated: 2010_08_28-PM-01_00_49 Last ObjectModification: 2010_04_16-PM-02_45_44 Home Index