Nuprl Lemma : geo_seg1_mk_seg_lemma
∀b,a:Top. (geo-seg1(ab) ~ a)
Proof
Definitions occuring in Statement :
geo-seg1: geo-seg1(s),
geo-mk-seg: ab,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
geo-mk-seg: ab,
geo-seg1: geo-seg1(s),
pi1: fst(t),
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation_alt,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}b,a:Top. (geo-seg1(ab) \msim{} a)
Date html generated:
2019_10_16-PM-01_14_43
Last ObjectModification:
2018_11_12-PM-03_12_31
Theory : euclidean!plane!geometry
Home
Index