Nuprl Lemma : geo-left-out-2

e:EuclideanPlane. ∀a,b,p,p':Point.  (p leftof ba  out(b pp')  p' leftof ba)


Proof




Definitions occuring in Statement :  geo-out: out(p ab) euclidean-plane: EuclideanPlane geo-left: leftof bc geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q geo-lsep: bc or: P ∨ Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} and: P ∧ Q cand: c∧ B geo-out: out(p ab) basic-geometry: BasicGeometry geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) top: Top int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A less_than: a < b squash: T true: True select: L[n] cons: [a b] subtract: m uimplies: supposing a
Lemmas referenced :  geo-left_wf colinear-lsep-cycle lsep-all-sym geo-sep-sym geo-colinear-is-colinear-set geo-out-colinear length_of_cons_lemma length_of_nil_lemma false_wf lelt_wf geo-out_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-point_wf left-convex left-implies-sep geo-between_wf not-left-and-right geo-sep_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut inlFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality because_Cache sqequalRule dependent_functionElimination independent_functionElimination productElimination isect_memberEquality voidElimination voidEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation imageMemberEquality baseClosed unionElimination instantiate independent_isectElimination inrFormation productEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,p,p':Point.    (p  leftof  ba  {}\mRightarrow{}  out(b  pp')  {}\mRightarrow{}  p'  leftof  ba)



Date html generated: 2017_10_02-PM-06_28_46
Last ObjectModification: 2017_09_29-PM-07_13_46

Theory : euclidean!plane!geometry


Home Index