### Nuprl Lemma : eu-colinear-cons

`∀e:EuclideanPlane. ∀L:Point List. ∀A:Point.`
`  (eu-colinear-set(e;[A / L]) `⇐⇒` eu-colinear-set(e;L) ∧ (∀B∈L.(∀C∈L.(¬(A = B ∈ Point)) `` Colinear(A;B;C))))`

Proof

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

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}L:Point  List.  \mforall{}A:Point.
(eu-colinear-set(e;[A  /  L])
\mLeftarrow{}{}\mRightarrow{}  eu-colinear-set(e;L)  \mwedge{}  (\mforall{}B\mmember{}L.(\mforall{}C\mmember{}L.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))

Date html generated: 2016_10_26-AM-07_43_45
Last ObjectModification: 2016_07_12-AM-08_11_02

Theory : euclidean!geometry

Home Index