### Nuprl Lemma : le_witness

`∀[i,j:ℤ]. ∀[x:i ≤ j].  (x = <λx.x, Ax, Ax> ∈ (i ≤ j))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` le: `A ≤ B` lambda: `λx.A[x]` pair: `<a, b>` int: `ℤ` equal: `s = t ∈ T` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False`
Lemmas referenced :  le_wf istype-int less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut hypothesis Error :universeIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :isect_memberEquality_alt,  axiomEquality because_Cache Error :inhabitedIsType,  productElimination equalityElimination independent_pairEquality Error :functionExtensionality_alt,  independent_functionElimination voidElimination

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[x:i  \mleq{}  j].    (x  =  <\mlambda{}x.x,  Ax,  Ax>)

Date html generated: 2019_06_20-AM-11_22_27
Last ObjectModification: 2018_10_01-PM-07_00_30

Theory : arithmetic

Home Index