Nuprl Lemma : right_endpoint_rccint_lemma

b,a:Top.  (right-endpoint([a, b]) b)


Proof




Definitions occuring in Statement :  rccint: [l, u] right-endpoint: right-endpoint(I) top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T right-endpoint: right-endpoint(I) pi2: snd(t) endpoints: endpoints(I) rccint: [l, u] outl: outl(x)
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}b,a:Top.    (right-endpoint([a,  b])  \msim{}  b)



Date html generated: 2016_05_18-AM-08_37_48
Last ObjectModification: 2015_12_27-PM-11_52_38

Theory : reals


Home Index