Nuprl Definition : satisfies-integer-inequality
xs ⋅ as ≥0 == (||xs|| = ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ) ∧ (as ⋅ xs ≥ 0 )
Definitions occuring in Statement :
integer-dot-product: as ⋅ bs,
hd: hd(l),
length: ||as||,
less_than: a < b,
ge: i ≥ j ,
and: P ∧ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
less_than: a < b,
length: ||as||,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
hd: hd(l),
ge: i ≥ j ,
integer-dot-product: as ⋅ bs,
natural_number: $n
FDL editor aliases :
sat-z-ge
Latex:
xs \mcdot{} as \mgeq{}0 == (||xs|| = ||as||) \mwedge{} 0 < ||xs|| \mwedge{} (hd(xs) = 1) \mwedge{} (as \mcdot{} xs \mgeq{} 0 )
Date html generated:
2016_05_14-AM-06_56_16
Last ObjectModification:
2015_09_22-PM-05_51_17
Theory : omega
Home
Index