Nuprl Lemma : member_rioint_lemma

r,u:Top.  (r ∈ (-∞u) r < u)


Proof




Definitions occuring in Statement :  rioint: (-∞u) i-member: r ∈ I rless: x < y top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T rioint: (-∞u) i-member: r ∈ I
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}r,u:Top.    (r  \mmember{}  (-\minfty{},  u)  \msim{}  r  <  u)



Date html generated: 2016_05_18-AM-08_37_04
Last ObjectModification: 2015_12_27-PM-11_52_27

Theory : reals


Home Index