Nuprl Definition : uni_sat_upto
a r !x:T. Q[x] == Q[a] ∧ (∀a':T. (Q[a'] ⇒ (a' [r] a)))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
binrel_ap: a [r] b
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
binrel_ap: a [r] b
Latex:
a r !x:T. Q[x] == Q[a] \mwedge{} (\mforall{}a':T. (Q[a'] {}\mRightarrow{} (a' [r] a)))
Date html generated:
2016_05_16-AM-07_45_06
Last ObjectModification:
2015_09_23-AM-09_51_56
Theory : factor_1
Home
Index