### Nuprl Lemma : eu-le-add1

`∀e:EuclideanPlane. ∀[p,q:{p:Point| O_X_p} ].  p ≤ p + q`

Proof

Definitions occuring in Statement :  eu-add-length: `p + q` eu-le: `p ≤ q` euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-X: `X` eu-O: `O` eu-point: `Point` 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]` eu-add-length: `p + q` eu-le: `p ≤ q` member: `t ∈ T` prop: `ℙ` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` implies: `P `` Q` not: `¬A` false: `False` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  set_wf eu-point_wf eu-between-eq_wf eu-O_wf eu-X_wf euclidean-plane_wf eu-not-colinear-OXY sq_stable__eu-between-eq eu-extend_wf subtype_rel_sets not_wf equal_wf eu-between-eq-same eu-extend-property eu-congruent_wf eu-between-eq-symmetry eu-between-eq-inner-trans eu-between-eq-exchange3
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule lambdaEquality because_Cache dependent_functionElimination productElimination applyEquality independent_isectElimination setEquality equalitySymmetry hyp_replacement Error :applyLambdaEquality,  equalityTransitivity independent_functionElimination voidElimination imageMemberEquality baseClosed imageElimination dependent_set_memberEquality productEquality equalityEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[p,q:\{p:Point|  O\_X\_p\}  ].    p  \mleq{}  p  +  q

Date html generated: 2016_10_26-AM-07_42_16
Last ObjectModification: 2016_07_12-AM-08_08_35

Theory : euclidean!geometry

Home Index