Nuprl Lemma : int_seg_properties

[i,j:ℤ]. ∀[y:{i..j-}].  i ≤ y < j

Proof

Definitions occuring in Statement :  int_seg: {i..j-} lelt: i ≤ j < k uall: [x:A]. B[x] int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_seg: {i..j-} prop: implies:  Q sq_stable: SqStable(P) uimplies: supposing a lelt: i ≤ j < k and: P ∧ Q squash: T le: A ≤ B not: ¬A false: False
Lemmas referenced :  int_seg_wf less_than'_wf squash_wf member-less_than sq_stable__less_than sq_stable__le less_than_wf le_wf sq_stable__and
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination hypothesisEquality hypothesis isect_memberEquality independent_functionElimination lambdaFormation because_Cache sqequalRule lambdaEquality dependent_functionElimination independent_isectElimination imageMemberEquality baseClosed imageElimination productElimination independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry intEquality voidElimination

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[y:\{i..j\msupminus{}\}].    i  \mleq{}  y  <  j

Date html generated: 2016_05_13-PM-04_02_04
Last ObjectModification: 2016_01_14-PM-07_24_36

Theory : int_1

Home Index