Nuprl Lemma : geo-length-null-segment
∀[e:BasicGeometry]. ∀[a:Point].  (|aa| = X ∈ Length)
Proof
Definitions occuring in Statement : 
geo-length: |s|
, 
geo-length-type: Length
, 
geo-mk-seg: ab
, 
basic-geometry: BasicGeometry
, 
geo-X: X
, 
geo-point: Point
, 
uall: ∀[x:A]. B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uimplies: b supposing a
, 
guard: {T}
, 
subtype_rel: A ⊆r B
, 
geo-zero-length: 0
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
Lemmas referenced : 
geo-primitives_wf, 
euclidean-plane-structure_wf, 
euclidean-plane_wf, 
basic-geometry_wf, 
subtype_rel_transitivity, 
basic-geometry-subtype, 
euclidean-plane-subtype, 
euclidean-plane-structure-subtype, 
geo-point_wf, 
trivial-zero-length
Rules used in proof : 
inhabitedIsType, 
isectIsTypeImplies, 
axiomEquality, 
isect_memberEquality_alt, 
independent_isectElimination, 
instantiate, 
applyEquality, 
universeIsType, 
hypothesisEquality, 
thin, 
isectElimination, 
sqequalHypSubstitution, 
extract_by_obid, 
hypothesis, 
sqequalRule, 
cut, 
introduction, 
isect_memberFormation_alt, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution
Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[a:Point].    (|aa|  =  X)
Date html generated:
2019_10_29-AM-09_13_50
Last ObjectModification:
2019_10_18-PM-03_16_32
Theory : euclidean!plane!geometry
Home
Index