Nuprl Lemma : int_sqrt_sq_exists_anne

n:. (r:{| (((r * r)  n)  n < (r + 1) * (r + 1))})


Proof




Definitions occuring in Statement :  nat: le: A  B all: x:A. B[x] sq_exists: x:{A| B[x]} and: P  Q multiply: n * m add: n + m natural_number: $n
Definitions :  rev_implies: P  Q iff: P  Q true: True squash: T lelt: i  j < k int_seg: {i..j} cand: A c B false: False not: A le: A  B nat: subtype_rel: A r B so_apply: x[s1;s2] so_lambda: x y.t[x; y] sq_exists: x:{A| B[x]} and: P  Q so_lambda: x.t[x] prop: member: t  T implies: P  Q all: x:A. B[x] so_apply: x[s] guard: {T} sq_type: SQType(T) uimplies: b supposing a uall: [x:A]. B[x] or: P  Q decidable: Dec(P)
Lemmas :  true_wf squash_wf decidable__lt int-value-type equal_wf set-value-type lelt_wf natrec_wf Error :less_than_wf,  le_wf nat_wf sq_exists_wf int_seg_wf all_wf int_subtype_base subtype_base_sq decidable__equal_int
\mforall{}n:\mBbbN{}.  (\mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))\})



Date html generated: 2014_03_27-PM-01_46_08
Last ObjectModification: 2014_03_26-AM-11_36_40

Home Index