Nuprl Lemma : eu-le_transitivity

e:EuclideanPlane. ∀[p,q,r:{p:Point| O_X_p} ].  (p ≤ r) supposing (q ≤ and p ≤ q)


Definitions occuring in Statement :  eu-le: p ≤ q euclidean-plane: EuclideanPlane eu-between-eq: a_b_c eu-X: X eu-O: O eu-point: Point uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] set: {x:A| B[x]} 
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] uimplies: supposing a eu-le: p ≤ q member: t ∈ T euclidean-plane: EuclideanPlane sq_stable: SqStable(P) implies:  Q squash: T prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  euclidean-plane_wf eu-O_wf eu-between-eq_wf eu-point_wf set_wf eu-le_wf eu-between-eq-exchange4 eu-between-eq-exchange3 eu-between-eq-inner-trans eu-between-eq-symmetry eu-X_wf sq_stable__eu-between-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation sqequalHypSubstitution cut lemma_by_obid dependent_functionElimination thin setElimination rename hypothesisEquality isectElimination hypothesis independent_functionElimination introduction because_Cache independent_isectElimination sqequalRule imageMemberEquality baseClosed imageElimination lambdaEquality

\mforall{}e:EuclideanPlane.  \mforall{}[p,q,r:\{p:Point|  O\_X\_p\}  ].    (p  \mleq{}  r)  supposing  (q  \mleq{}  r  and  p  \mleq{}  q)

Date html generated: 2016_05_18-AM-06_37_23
Last ObjectModification: 2016_01_16-PM-10_30_30

Theory : euclidean!geometry

Home Index