Nuprl Definition : oal_lt
ps << qs == ∃k:|s|. ((∀k':|s|. ((k <s k')
⇒ ((ps[k']) = (qs[k']) ∈ |g|))) ∧ ((ps[k]) < (qs[k])))
Definitions occuring in Statement :
lookup: as[k]
,
all: ∀x:A. B[x]
,
exists: ∃x:A. B[x]
,
implies: P
⇒ Q
,
and: P ∧ Q
,
equal: s = t ∈ T
,
grp_lt: a < b
,
grp_id: e
,
grp_car: |g|
,
set_lt: a <p b
,
set_car: |p|
Definitions occuring in definition :
exists: ∃x:A. B[x]
,
and: P ∧ Q
,
all: ∀x:A. B[x]
,
set_car: |p|
,
implies: P
⇒ Q
,
set_lt: a <p b
,
equal: s = t ∈ T
,
grp_car: |g|
,
grp_lt: a < b
,
lookup: as[k]
,
grp_id: e
Latex:
ps << qs == \mexists{}k:|s|. ((\mforall{}k':|s|. ((k <s k') {}\mRightarrow{} ((ps[k']) = (qs[k'])))) \mwedge{} ((ps[k]) < (qs[k])))
Date html generated:
2016_05_16-AM-08_20_48
Last ObjectModification:
2015_09_23-AM-09_53_07
Theory : polynom_2
Home
Index