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