Nuprl Lemma : rcoint_wf

[l,u:ℝ].  ([l, u) ∈ Interval)


Proof




Definitions occuring in Statement :  rcoint: [l, u) interval: Interval real: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  rcoint: [l, u) interval: Interval uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  real_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairEquality inlEquality hypothesisEquality lemma_by_obid hypothesis inrEquality sqequalHypSubstitution axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality isectElimination thin because_Cache

Latex:
\mforall{}[l,u:\mBbbR{}].    ([l,  u)  \mmember{}  Interval)



Date html generated: 2016_05_18-AM-08_20_22
Last ObjectModification: 2015_12_27-PM-11_55_25

Theory : reals


Home Index