Nuprl Lemma : decidable__q-constraints-squash
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:{ℚ List| q-constraints(k;A;y)})
Proof
Definitions occuring in Statement : 
q-constraints: q-constraints(k;A;y)
, 
rationals: ℚ
, 
list: T List
, 
nat: ℕ
, 
decidable: Dec(P)
, 
all: ∀x:A. B[x]
, 
sq_exists: ∃x:{A| B[x]}
, 
function: x:A ⟶ B[x]
, 
product: x:A × B[x]
, 
int: ℤ
Lemmas referenced : 
decidable__q-constraints
Rules used in proof : 
cut, 
lemma_by_obid, 
hypothesis
Latex:
\mforall{}k:\mBbbN{}.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.    Dec(\mexists{}y:\{\mBbbQ{}  List|  q-constraints(k;A;y)\})
Date html generated:
2016_05_15-PM-11_31_08
Last ObjectModification:
2015_12_27-PM-07_29_46
Theory : rationals
Home
Index