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:  Q false: False squash: T cand: c∧ B sq_exists: x:A [B[x]] rv-congruent: ab=cd subtype_rel: A ⊆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