Nuprl Lemma : le_to_lt_rw
∀[i,j:ℤ]. {uiff(i ≤ j;i < j + 1)}
Proof
Definitions occuring in Statement :
less_than: a < b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
guard: {T},
le: A ≤ B,
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
le_to_lt
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}[i,j:\mBbbZ{}]. \{uiff(i \mleq{} j;i < j + 1)\}
Date html generated:
2016_05_14-AM-07_20_23
Last ObjectModification:
2015_12_26-PM-01_32_25
Theory : int_2
Home
Index