Nuprl Lemma : geo-left-out

e:EuclideanPlane. ∀a,b,a',p:Point.  (p leftof ba  out(b aa')  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] member: t ∈ T implies:  Q geo-out: out(p ab) and: P ∧ Q not: ¬A geo-sep: a ≠ b cand: c∧ B prop: uall: [x:A]. B[x] subtype_rel: A ⊆B basic-geometry: BasicGeometry guard: {T} uimplies: supposing a
Lemmas referenced :  geo-left-out-better not_wf geo-between_wf geo-out_wf geo-left_wf geo-point_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination productElimination sqequalRule independent_pairFormation productEquality isectElimination applyEquality because_Cache instantiate independent_isectElimination

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



Date html generated: 2018_05_22-AM-11_59_06
Last ObjectModification: 2018_04_20-PM-01_53_31

Theory : euclidean!plane!geometry


Home Index