Nuprl Definition : ts-stable-rel
ts-stable-rel(ts;x,y.R[x; y]) == ∀x,y:ts-type(ts). ((x (ts-rel(ts)^*) y) ⇒ R[x; y])
Definitions occuring in Statement :
ts-rel: ts-rel(ts),
ts-type: ts-type(ts),
rel_star: R^*,
infix_ap: x f y,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
infix_ap: x f y,
rel_star: R^*,
ts-type: ts-type(ts),
ts-rel: ts-rel(ts)
FDL editor aliases :
ts-stable-rel
Latex:
ts-stable-rel(ts;x,y.R[x; y]) ==
\mforall{}x,y:ts-type(ts). ((x (ts-rel(ts)\^{}*) y) {}\mRightarrow{} R[x; y])
Date html generated:
2016_05_15-PM-05_43_10
Last ObjectModification:
2015_09_23-AM-07_58_22
Theory : general
Home
Index