Nuprl Lemma : geo-le-null-segment
∀e:BasicGeometry. ∀[p:Length]. ∀[a:Point]. uiff(p ≤ |aa|;p = |aa| ∈ Length)
Proof
Definitions occuring in Statement :
geo-le: p ≤ q,
geo-length: |s|,
geo-length-type: Length,
geo-mk-seg: ab,
basic-geometry: BasicGeometry,
geo-point: Point,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
basic-geometry: BasicGeometry,
euclidean-plane: EuclideanPlane,
uiff: uiff(P;Q),
and: P ∧ Q,
prop: ℙ,
squash: ↓T,
true: True,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
sq_stable: SqStable(P),
geo-length-type: Length,
quotient: x,y:A//B[x; y],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2]
Lemmas referenced :
subtype-geo-length-type,
geo-point_wf,
euclidean-plane-structure-subtype,
euclidean-plane-subtype,
basic-geometry-subtype,
subtype_rel_transitivity,
basic-geometry_wf,
euclidean-plane_wf,
euclidean-plane-structure_wf,
geo-primitives_wf,
geo-length-type_wf,
geo-le_wf,
geo-length_wf,
geo-mk-seg_wf,
equal_wf,
geo-between-trivial,
geo-O_wf,
geo-X_wf,
geo-between_wf,
squash_wf,
true_wf,
geo-length-null-segment,
iff_weakening_equal,
sq_stable__geo-le,
sq_stable__uiff,
sq_stable__equal,
geo-le_weakening,
equal-wf-base,
geo-eq_wf,
geo-le_imp,
quotient-member-eq,
geo-length-equiv,
geo-between-same,
geo-eq_inversion
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
instantiate,
independent_isectElimination,
sqequalRule,
setElimination,
rename,
because_Cache,
independent_pairFormation,
dependent_functionElimination,
dependent_set_memberEquality,
lambdaEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
universeEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed,
productElimination,
independent_functionElimination,
pointwiseFunctionalityForEquality,
pertypeElimination,
productEquality,
setEquality,
promote_hyp
Latex:
\mforall{}e:BasicGeometry. \mforall{}[p:Length]. \mforall{}[a:Point]. uiff(p \mleq{} |aa|;p = |aa|)
Date html generated:
2017_10_02-PM-04_53_53
Last ObjectModification:
2017_08_17-PM-01_28_24
Theory : euclidean!plane!geometry
Home
Index