Nuprl Definition : uni_sat_upto

!x:T. Q[x]  ==  Q[a] ∧ (∀a':T. (Q[a']  (a' [r] a)))



Definitions occuring in Statement :  all: x:A. B[x] implies:  Q and: P ∧ Q binrel_ap: [r] b
Definitions occuring in definition :  and: P ∧ Q all: x:A. B[x] implies:  Q binrel_ap: [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