Nuprl Definition : rel_finite
rel_finite(T;R) ==  ∀x:T. ∃L:T List. ∀z:T. ((z R x) 
⇒ (z ∈ L))
Definitions occuring in Statement : 
l_member: (x ∈ l)
, 
list: T List
, 
infix_ap: x f y
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
implies: P 
⇒ Q
Definitions occuring in definition : 
exists: ∃x:A. B[x]
, 
list: T List
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
infix_ap: x f 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