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