Nuprl Lemma : geo-out-strict-colinear

e:BasicGeometry. ∀a,b,c:Point.  (geo-out-strict(e;a;b;c)  Colinear(a;b;c))


Proof




Definitions occuring in Statement :  geo-out-strict: geo-out-strict(e;p;a;b) basic-geometry: BasicGeometry geo-colinear: Colinear(a;b;c) geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q geo-colinear: Colinear(a;b;c) not: ¬A geo-out-strict: geo-out-strict(e;p;a;b) and: P ∧ Q cand: c∧ B member: t ∈ T basic-geometry: BasicGeometry uall: [x:A]. B[x] uimplies: supposing a guard: {T} geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] prop: false: False select: L[n] cons: [a b] subtract: m subtype_rel: A ⊆B

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (geo-out-strict(e;a;b;c)  {}\mRightarrow{}  Colinear(a;b;c))



Date html generated: 2020_05_20-AM-09_54_50
Last ObjectModification: 2019_12_23-AM-10_14_41

Theory : euclidean!plane!geometry


Home Index