Nuprl Lemma : geo-cong-preserves-lt
∀e:BasicGeometry. ∀p,q,p1,q1:Length.  (p < q 
⇒ (p = p1 ∈ Length) 
⇒ (q = q1 ∈ Length) 
⇒ p1 < q1)
Proof
Definitions occuring in Statement : 
geo-lt: p < q
, 
geo-length-type: Length
, 
basic-geometry: BasicGeometry
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
member: t ∈ T
, 
squash: ↓T
, 
uall: ∀[x:A]. B[x]
, 
true: True
Lemmas referenced : 
geo-lt_wf, 
squash_wf, 
true_wf, 
geo-length-type_wf, 
basic-geometry_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation_alt, 
cut, 
hypothesis, 
hyp_replacement, 
thin, 
equalitySymmetry, 
sqequalRule, 
applyEquality, 
lambdaEquality_alt, 
sqequalHypSubstitution, 
imageElimination, 
introduction, 
extract_by_obid, 
isectElimination, 
hypothesisEquality, 
equalityTransitivity, 
universeIsType, 
inhabitedIsType, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
equalityIstype, 
because_Cache
Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q,p1,q1:Length.    (p  <  q  {}\mRightarrow{}  (p  =  p1)  {}\mRightarrow{}  (q  =  q1)  {}\mRightarrow{}  p1  <  q1)
Date html generated:
2019_10_16-PM-01_19_09
Last ObjectModification:
2019_03_04-PM-04_21_09
Theory : euclidean!plane!geometry
Home
Index