Nuprl Lemma : r2-compass-compass-simple1
∀a,b:ℝ^2. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2|
↓∃p,q:ℝ^2
((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d)))
∧ cd=cq
∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))} .
(∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))])
Proof
Definitions occuring in Statement :
r2-left: r2-left(p;q;r),
rv-be: a_b_c,
real-vec-sep: a ≠ b,
rv-congruent: ab=cd,
real-vec: ℝ^n,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
exists: ∃x:A. B[x],
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
not: ¬A,
implies: P ⇒ Q,
false: False,
squash: ↓T,
cand: A c∧ B,
sq_exists: ∃x:A [B[x]],
rv-congruent: ab=cd,
subtype_rel: A ⊆r B,
sq_stable: SqStable(P)
Latex:
\mforall{}a,b:\mBbbR{}\^{}2. \mforall{}c:\{c:\mBbbR{}\^{}2| a \mneq{} c\} . \mforall{}d:\{d:\mBbbR{}\^{}2|
\mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
((ab=ap \mwedge{} (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2. (c\_w\_d \mwedge{} cw=cp \mwedge{} w \mneq{} d)))
\mwedge{} cd=cq
\mwedge{} (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2. (a\_w\_b \mwedge{} aw=aq \mwedge{} w \mneq{} b)))\} .
(\mexists{}u:\mBbbR{}\^{}2 [(ab=au \mwedge{} cd=cu \mwedge{} r2-left(u;a;c))])
Date html generated:
2020_05_20-PM-01_01_33
Last ObjectModification:
2019_12_11-PM-00_28_18
Theory : reals
Home
Index