Nuprl Lemma : member_rccint_lemma

r,u,l:Top.  (r ∈ [l, u] (l ≤ r) ∧ (r ≤ u))


Proof




Definitions occuring in Statement :  rccint: [l, u] i-member: r ∈ I rleq: x ≤ y top: Top all: x:A. B[x] and: P ∧ Q sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T rccint: [l, 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,l:Top.    (r  \mmember{}  [l,  u]  \msim{}  (l  \mleq{}  r)  \mwedge{}  (r  \mleq{}  u))



Date html generated: 2016_05_18-AM-08_20_04
Last ObjectModification: 2015_12_27-PM-11_55_54

Theory : reals


Home Index