Nuprl Lemma : eu-inner-pasch_wf

[e:EuclideanStructure]. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ]\000C.
  (eu-inner-pasch(e;a;b;c;p;q) ∈ Point)


Proof




Definitions occuring in Statement :  eu-inner-pasch: eu-inner-pasch(e;a;b;c;p;q) eu-between-eq: a_b_c eu-colinear: Colinear(a;b;c) eu-between: a-b-c eu-point: Point euclidean-structure: EuclideanStructure uall: [x:A]. B[x] not: ¬A member: t ∈ T set: {x:A| B[x]} 
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eu-inner-pasch: eu-inner-pasch(e;a;b;c;p;q) eu-between-eq: a_b_c eu-point: Point eu-between: a-b-c eu-colinear: Colinear(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 and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q implies:  Q uimplies: supposing a all: x:A. B[x]
Lemmas referenced :  subtype_rel_self not_wf equal_wf uall_wf iff_wf and_wf isect_wf set_wf eu-point_wf eu-between-eq_wf eu-between_wf eu-colinear_wf euclidean-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule sqequalHypSubstitution dependentIntersectionElimination dependentIntersectionEqElimination hypothesis applyEquality tokenEquality instantiate lemma_by_obid isectElimination universeEquality functionEquality equalityTransitivity equalitySymmetry lambdaEquality cumulativity hypothesisEquality because_Cache setEquality productEquality productElimination lambdaFormation dependent_set_memberEquality axiomEquality isect_memberEquality

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].  \mforall{}[p:\{p:Point|  a-p-c\}  ].
\mforall{}[q:\{q:Point|  b\_q\_c\}  ].
    (eu-inner-pasch(e;a;b;c;p;q)  \mmember{}  Point)



Date html generated: 2016_05_18-AM-06_33_19
Last ObjectModification: 2015_12_28-AM-09_28_20

Theory : euclidean!geometry


Home Index