### Nuprl Lemma : le_witness_for_triv

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

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` member: `t ∈ T` lambda: `λx.A[x]` pair: `<a, b>` int: `ℤ` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` top: `Top` not: `¬A` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  member-not less_than'_wf istype-void istype-le istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule independent_pairEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :isect_memberEquality_alt,  voidElimination independent_isectElimination Error :lambdaFormation_alt,  Error :universeIsType,  axiomEquality equalityTransitivity equalitySymmetry Error :isectIsTypeImplies,  Error :inhabitedIsType,  productElimination independent_functionElimination

Latex:
\mforall{}[i,j:\mBbbZ{}].    <\mlambda{}x.Ax,  Ax,  Ax>  \mmember{}  i  \mleq{}  j  supposing  i  \mleq{}  j

Date html generated: 2019_06_20-AM-11_22_25
Last ObjectModification: 2018_10_27-PM-10_32_52

Theory : arithmetic

Home Index