Nuprl Definition : q-constraints

q-constraints(k;A;y) ==  (||y|| = k ∈ ℤ) c∧ (∀xr∈A.q-rel(snd(xr);q-linear(k;j.(fst(xr)) j;y)))



Definitions occuring in Statement :  q-rel: q-rel(r;x),  q-linear: q-linear(k;i.X[i];y),  l_all: (∀x∈L.P[x]),  length: ||as||,  cand: A c∧ B,  pi1: fst(t),  pi2: snd(t),  apply: f a,  int: ℤ,  equal: s = t ∈ T
Definitions occuring in definition :  cand: A c∧ B,  equal: s = t ∈ T,  int: ℤ,  length: ||as||,  l_all: (∀x∈L.P[x]),  q-rel: q-rel(r;x),  pi2: snd(t),  q-linear: q-linear(k;i.X[i];y),  apply: f a,  pi1: fst(t)
FDL editor aliases :  q-constraints

Latex:
q-constraints(k;A;y)  ==    (||y||  =  k)  c\mwedge{}  (\mforall{}xr\mmember{}A.q-rel(snd(xr);q-linear(k;j.(fst(xr))  j;y)))



Date html generated: 2016_05_15-PM-11_19_12
Last ObjectModification: 2015_09_23-AM-08_28_25

Theory : rationals


Home Index