Nuprl Lemma : eu-length_wf

`∀[e:EuclideanPlane]. ∀[s:Segment].  (|s| ∈ {p:Point| O_X_p} )`

Proof

Definitions occuring in Statement :  eu-length: `|s|` eu-segment: `Segment` euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-X: `X` eu-O: `O` eu-point: `Point` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} `
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` eu-length: `|s|` all: `∀x:A. B[x]` euclidean-plane: `EuclideanPlane` and: `P ∧ Q` prop: `ℙ`
Lemmas referenced :  eu-extend-property eu-O_wf eu-not-colinear-OXY eu-X_wf not_wf equal_wf eu-point_wf eu-seg1_wf eu-seg2_wf eu-extend_wf eu-between-eq_wf eu-segment_wf euclidean-plane_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination setElimination rename hypothesis because_Cache productElimination dependent_set_memberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[s:Segment].    (|s|  \mmember{}  \{p:Point|  O\_X\_p\}  )

Date html generated: 2016_10_26-AM-07_41_37
Last ObjectModification: 2016_09_20-AM-10_56_33

Theory : euclidean!geometry

Home Index