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