### Nuprl Lemma : eu-line-circle_wf

`∀[e:EuclideanStructure]. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ].`
`∀[q:{q:Point| aq=ay ∧ (¬(q = p ∈ Point))} ].`
`  (intersect pq (at radius xy) with Oab  ∈ Point × Point)`

Proof

Definitions occuring in Statement :  eu-line-circle: `intersect pq (at radius xy) with Oab ` eu-between-eq: `a_b_c` eu-congruent: `ab=cd` eu-point: `Point` euclidean-structure: `EuclideanStructure` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` product: `x:A × B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` eu-line-circle: `intersect pq (at radius xy) with Oab ` and: `P ∧ Q` eu-point: `Point` eu-congruent: `ab=cd` eu-between-eq: `a_b_c` euclidean-structure: `EuclideanStructure` record+: record+ record-select: `r.x` subtype_rel: `A ⊆r B` eq_atom: `x =a y` ifthenelse: `if b then t else f fi ` btrue: `tt` guard: `{T}` prop: `ℙ` spreadn: spread3 so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` uimplies: `b supposing a` all: `∀x:A. B[x]` cand: `A c∧ B`
Lemmas referenced :  subtype_rel_self not_wf equal_wf uall_wf iff_wf and_wf isect_wf set_wf eu-point_wf eu-congruent_wf eu-between-eq_wf euclidean-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule sqequalHypSubstitution productElimination dependentIntersectionElimination dependentIntersectionEqElimination hypothesis applyEquality tokenEquality instantiate lemma_by_obid isectElimination universeEquality functionEquality equalityTransitivity equalitySymmetry lambdaEquality cumulativity hypothesisEquality because_Cache setEquality productEquality lambdaFormation dependent_set_memberEquality independent_pairFormation axiomEquality isect_memberEquality

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b:Point].  \mforall{}[x:\{x:Point|  a\_x\_b\}  ].  \mforall{}[y:\{y:Point|  a\_b\_y\}  ].  \mforall{}[p:\{p:Point|\000C
ap=ax\}  ].
\mforall{}[q:\{q:Point|  aq=ay  \mwedge{}  (\mneg{}(q  =  p))\}  ].
(intersect  pq  (at  radius  xy)  with  Oab    \mmember{}  Point  \mtimes{}  Point)

Date html generated: 2016_05_18-AM-06_33_23
Last ObjectModification: 2015_12_28-AM-09_28_18

Theory : euclidean!geometry

Home Index