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