Nuprl Definition : rel_finite

rel_finite(T;R) ==  ∀x:T. ∃L:T List. ∀z:T. ((z x)  (z ∈ L))



Definitions occuring in Statement :  l_member: (x ∈ l) list: List infix_ap: y all: x:A. B[x] exists: x:A. B[x] implies:  Q
Definitions occuring in definition :  exists: x:A. B[x] list: List all: x:A. B[x] implies:  Q infix_ap: y l_member: (x ∈ l)
FDL editor aliases :  rel_finite

Latex:
rel\_finite(T;R)  ==    \mforall{}x:T.  \mexists{}L:T  List.  \mforall{}z:T.  ((z  R  x)  {}\mRightarrow{}  (z  \mmember{}  L))



Date html generated: 2016_05_14-PM-03_51_44
Last ObjectModification: 2015_09_22-PM-06_01_46

Theory : relations2


Home Index