### Nuprl Lemma : eu-colinear-append

`∀e:EuclideanPlane. ∀L1,L2:Point List.`
`  ((∃A,B:Point. ((¬(A = B ∈ Point)) ∧ ((A ∈ L1) ∧ (A ∈ L2)) ∧ (B ∈ L1) ∧ (B ∈ L2)))`
`  `` eu-colinear-set(e;L1)`
`  `` eu-colinear-set(e;L2)`
`  `` eu-colinear-set(e;L1 @ L2))`

Proof

Definitions occuring in Statement :  eu-colinear-set: `eu-colinear-set(e;L)` euclidean-plane: `EuclideanPlane` eu-point: `Point` l_member: `(x ∈ l)` append: `as @ bs` list: `T List` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` and: `P ∧ Q` eu-colinear-set: `eu-colinear-set(e;L)` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` guard: `{T}` stable: `Stable{P}` uimplies: `b supposing a` not: `¬A` or: `P ∨ Q` false: `False`
Lemmas referenced :  eu-colinear-set_wf exists_wf eu-point_wf not_wf equal_wf l_member_wf list_wf euclidean-plane_wf l_all_iff l_all_wf2 eu-colinear_wf all_wf l_all_append append_wf stable__colinear false_wf or_wf minimal-double-negation-hyp-elim minimal-not-not-excluded-middle eu-colinear-transitivity eu-colinear-cycle eu-colinear-swap eu-colinear-def member_wf eu-between_wf eu-colinear-permute
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis setElimination rename because_Cache sqequalRule lambdaEquality productEquality addLevel dependent_functionElimination functionEquality setEquality independent_functionElimination allFunctionality levelHypothesis promote_hyp independent_pairFormation impliesFunctionality allLevelFunctionality impliesLevelFunctionality independent_isectElimination unionElimination voidElimination hyp_replacement equalitySymmetry Error :applyLambdaEquality,  equalityTransitivity

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}L1,L2:Point  List.
((\mexists{}A,B:Point.  ((\mneg{}(A  =  B))  \mwedge{}  ((A  \mmember{}  L1)  \mwedge{}  (A  \mmember{}  L2))  \mwedge{}  (B  \mmember{}  L1)  \mwedge{}  (B  \mmember{}  L2)))
{}\mRightarrow{}  eu-colinear-set(e;L1)
{}\mRightarrow{}  eu-colinear-set(e;L2)
{}\mRightarrow{}  eu-colinear-set(e;L1  @  L2))

Date html generated: 2016_10_26-AM-07_44_03
Last ObjectModification: 2016_07_12-AM-08_11_29

Theory : euclidean!geometry

Home Index