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)


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: 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 ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt guard: {T} prop: spreadn: spread3 so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q implies:  Q uimplies: supposing a all: x:A. B[x] cand: 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

\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