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: 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