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