Nuprl Lemma : geo-col-connect

e:BasicGeometry. ∀a,b,c,d:Point.  (c ≠  Colinear(a;b;c)  Colinear(c;b;d)  Colinear(a;b;d))


Proof




Definitions occuring in Statement :  basic-geometry: BasicGeometry geo-colinear: Colinear(a;b;c) geo-sep: a ≠ b geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  basic-geometry: BasicGeometry subtract: m cons: [a b] select: L[n] true: True squash: T less_than: a < b not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B lelt: i ≤ j < k int_seg: {i..j-} l_all: (∀x∈L.P[x]) geo-colinear-set: geo-colinear-set(e; L) so_apply: x[s1;s2;s3] top: Top so_lambda: so_lambda(x,y,z.t[x; y; z]) append: as bs so_apply: x[s] so_lambda: λ2x.t[x] prop: or: P ∨ Q rev_implies:  Q iff: ⇐⇒ Q cand: c∧ B and: P ∧ Q exists: x:A. B[x] uimplies: supposing a guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] member: t ∈ T implies:  Q all: x:A. B[x]
Lemmas referenced :  geo-colinear_wf lelt_wf false_wf length_of_nil_lemma length_of_cons_lemma list_ind_nil_lemma list_ind_cons_lemma geo-colinear-is-colinear-set exists_wf geo-sep_wf equal_wf l_member_wf cons_member nil_wf Error :basic-geo-primitives_wf,  Error :basic-geo-structure_wf,  basic-geometry_wf subtype_rel_transitivity basic-geometry-subtype geo-point_wf cons_wf geo-colinear-append
Rules used in proof :  rename setElimination baseClosed imageMemberEquality natural_numberEquality dependent_set_memberEquality voidEquality voidElimination isect_memberEquality lambdaEquality productEquality inlFormation inrFormation productElimination independent_pairFormation dependent_pairFormation independent_functionElimination because_Cache sqequalRule independent_isectElimination instantiate hypothesis applyEquality isectElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (c  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  Colinear(c;b;d)  {}\mRightarrow{}  Colinear(a;b;d))



Date html generated: 2017_10_02-PM-06_40_06
Last ObjectModification: 2017_08_05-PM-04_46_46

Theory : euclidean!plane!geometry


Home Index