### 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: List uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  so_apply: x[s] implies:  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