Nuprl Lemma : geo-triangles-between

e:HeytingGeometry. ∀a,b,c,p,q:Point.  (a bc  b-p-a  b-q-c  bq)


Proof




Definitions occuring in Statement :  geo-triangle: bc heyting-geometry: HeytingGeometry geo-strict-between: a-b-c geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  heyting-geometry: Error :heyting-geometry,  uimplies: supposing a guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] prop: member: t ∈ T implies:  Q all: x:A. B[x] 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-} top: Top l_all: (∀x∈L.P[x]) geo-colinear-set: geo-colinear-set(e; L) cand: c∧ B and: P ∧ Q
Lemmas referenced :  geo-point_wf Error :geo-triangle_wf,  Error :basic-geo-primitives_wf,  Error :basic-geo-structure_wf,  basic-geometry_wf Error :heyting-geometry_wf,  subtype_rel_transitivity heyting-geometry-subtype basic-geometry-subtype geo-strict-between_wf geo-strict-between-sep2 geo-sep-sym lelt_wf false_wf length_of_nil_lemma length_of_cons_lemma geo-strict-between-implies-colinear geo-colinear-is-colinear-set geo-triangle-separation
Rules used in proof :  rename setElimination because_Cache sqequalRule independent_isectElimination instantiate hypothesis applyEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination baseClosed imageMemberEquality independent_pairFormation natural_numberEquality dependent_set_memberEquality voidEquality voidElimination isect_memberEquality independent_functionElimination dependent_functionElimination

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,p,q:Point.    (a  \#  bc  {}\mRightarrow{}  b-p-a  {}\mRightarrow{}  b-q-c  {}\mRightarrow{}  p  \#  bq)



Date html generated: 2017_10_02-PM-07_03_20
Last ObjectModification: 2017_08_08-PM-00_41_14

Theory : euclidean!plane!geometry


Home Index