### Nuprl Lemma : eu-colinear-set_wf

`∀[e:EuclideanPlane]. ∀[L:Point List].  (eu-colinear-set(e;L) ∈ ℙ)`

Proof

Definitions occuring in Statement :  eu-colinear-set: `eu-colinear-set(e;L)` euclidean-plane: `EuclideanPlane` eu-point: `Point` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` so_lambda: `λ2x.t[x]` euclidean-plane: `EuclideanPlane` eu-colinear-set: `eu-colinear-set(e;L)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  l_all_wf2 eu-point_wf l_member_wf not_wf equal_wf eu-colinear_wf list_wf euclidean-plane_wf
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality dependent_functionElimination setEquality functionEquality because_Cache lambdaFormation lambdaEquality hypothesis hypothesisEquality rename setElimination thin isectElimination sqequalHypSubstitution lemma_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[L:Point  List].    (eu-colinear-set(e;L)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_18-AM-06_40_18
Last ObjectModification: 2016_01_03-PM-01_52_08

Theory : euclidean!geometry

Home Index