Nuprl Lemma : rv-circle-circle-lemma2'
∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:ℝ^2.
((r0 < ||b||)
⇒ ((r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2))
⇒ (∃u,v:ℝ^2
(((||u|| = r1) ∧ (||u - b|| = r2))
∧ ((||v|| = r1) ∧ (||v - b|| = r2))
∧ (((r1^2 - r2^2) + ||b||^2^2 < (r(4) * ||b||^2 * r1^2)) ⇒ (r2-left(u;b;λi.r0) ∧ r2-left(v;λi.r0;b))))))
Proof
Definitions occuring in Statement :
r2-left: r2-left(p;q;r),
real-vec-norm: ||x||,
real-vec-sub: X - Y,
real-vec: ℝ^n,
rleq: x ≤ y,
rless: x < y,
rnexp: x^k1,
rsub: x - y,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
lambda: λx.A[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
not: ¬A,
implies: P ⇒ Q,
false: False,
uall: ∀[x:A]. B[x],
prop: ℙ,
dot-product: x⋅y,
subtract: n - m,
so_lambda: λ2x.t[x],
real-vec: ℝ^n,
int_seg: {i..j-},
lelt: i ≤ j < k,
less_than: a < b,
squash: ↓T,
rless: x < y,
sq_exists: ∃x:A [B[x]],
nat_plus: ℕ+,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
so_apply: x[s],
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
uiff: uiff(P;Q),
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
eq_int: (i =z j),
nequal: a ≠ b ∈ T ,
lt_int: i <z j,
rev_uimplies: rev_uimplies(P;Q),
req_int_terms: t1 ≡ t2,
rneq: x ≠ y,
true: True,
rdiv: (x/y),
exp: i^n,
primrec: primrec(n;b;c),
primtailrec: primtailrec(n;i;b;f),
subtype_rel: A ⊆r B,
let: let,
sq_stable: SqStable(P),
nonneg-poly: nonneg-poly(p),
bl-all: (∀x∈L.P[x])_b,
reduce: reduce(f;k;as),
list_ind: list_ind,
int_term_to_ipoly: int_term_to_ipoly(t),
int_term_ind: int_term_ind,
itermAdd: left (+) right,
add_ipoly: add_ipoly(p;q),
add-ipoly-prepend: add-ipoly-prepend(p;q;l),
itermMultiply: left (*) right,
mul_ipoly: mul_ipoly(p;q),
itermVar: vvar,
cons: [a / b],
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
nil: [],
mul-mono-poly: mul-mono-poly(m;p),
mul-monomials: mul-monomials(m1;m2),
merge-int-accum: merge-int-accum(as;bs),
eager-accum: eager-accum(x,a.f[x; a];y;l),
callbyvalueall: callbyvalueall,
evalall: evalall(t),
insert-int: insert-int(x;l),
imonomial-le: imonomial-le(m1;m2),
intlex: l1 ≤_lex l2,
length: ||as||,
pi2: snd(t),
bor: p ∨bq,
band: p ∧b q,
intlex-aux: intlex-aux(l1;l2),
rev-append: rev(as) + bs,
list_accum: list_accum,
nonneg-monomial: nonneg-monomial(m),
le_int: i ≤z j,
even-int-list: even-int-list(L),
null: null(as),
tl: tl(l),
hd: hd(l),
pi1: fst(t),
real-vec-norm: ||x||,
cand: A c∧ B,
real-vec-mul: a*X,
real-vec-add: X + Y,
r2-left: r2-left(p;q;r),
r2-det: |pqr|,
real-vec-sub: X - Y
Latex:
\mforall{}r1,r2:\{r:\mBbbR{}| r0 \mleq{} r\} . \mforall{}b:\mBbbR{}\^{}2.
((r0 < ||b||)
{}\mRightarrow{} ((r1\^{}2 - r2\^{}2) + ||b||\^{}2\^{}2 \mleq{} (r(4) * ||b||\^{}2 * r1\^{}2))
{}\mRightarrow{} (\mexists{}u,v:\mBbbR{}\^{}2
(((||u|| = r1) \mwedge{} (||u - b|| = r2))
\mwedge{} ((||v|| = r1) \mwedge{} (||v - b|| = r2))
\mwedge{} (((r1\^{}2 - r2\^{}2) + ||b||\^{}2\^{}2 < (r(4) * ||b||\^{}2 * r1\^{}2))
{}\mRightarrow{} (r2-left(u;b;\mlambda{}i.r0) \mwedge{} r2-left(v;\mlambda{}i.r0;b))))))
Date html generated:
2020_05_20-PM-01_00_12
Last ObjectModification:
2019_12_14-PM-02_58_25
Theory : reals
Home
Index