Nuprl Lemma : rciint_wf

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


Proof




Definitions occuring in Statement :  rciint: [l, ∞) interval: Interval real: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  rciint: [l, ∞) interval: Interval uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B top: Top
Lemmas referenced :  real_wf top_wf it_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairEquality inlEquality hypothesisEquality lemma_by_obid hypothesis inrEquality applyEquality thin lambdaEquality isect_memberEquality voidElimination voidEquality sqequalHypSubstitution unionEquality axiomEquality equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_18-AM-08_20_48
Last ObjectModification: 2015_12_27-PM-11_55_16

Theory : reals


Home Index