### Nuprl Lemma : eu-le_transitivity

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

Proof

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: `b 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: `b supposing a` eu-le: `p ≤ q` member: `t ∈ T` euclidean-plane: `EuclideanPlane` sq_stable: `SqStable(P)` implies: `P `` 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

Latex:
\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