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