Nuprl Lemma : eu-colinear_wf

[e:EuclideanStructure]. ∀[a,b,c:Point].  (Colinear(a;b;c) ∈ ℙ)


Proof




Definitions occuring in Statement :  eu-colinear: Colinear(a;b;c) eu-point: Point euclidean-structure: EuclideanStructure uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eu-colinear: Colinear(a;b;c) eu-point: Point 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 eu-point_wf euclidean-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution dependentIntersectionElimination dependentIntersectionEqElimination thin hypothesis applyEquality tokenEquality instantiate lemma_by_obid isectElimination universeEquality functionEquality equalityTransitivity equalitySymmetry lambdaEquality cumulativity hypothesisEquality because_Cache setEquality productEquality productElimination setElimination rename lambdaFormation axiomEquality isect_memberEquality

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b,c:Point].    (Colinear(a;b;c)  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-06_32_29
Last ObjectModification: 2015_12_28-AM-09_28_41

Theory : euclidean!geometry


Home Index