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