Nuprl Lemma : nc-e-comp-nc-1

[I:fset(ℕ)]. ∀[i,j:{j:ℕ| ¬j ∈ I} ].  ((i1) e(i;j) ⋅ (j1) ∈ I ⟶ I+i)


Proof




Definitions occuring in Statement :  nc-e: e(i;j) nc-1: (i1) add-name: I+i nh-comp: g ⋅ f names-hom: I ⟶ J fset-member: a ∈ s fset: fset(T) int-deq: IntDeq nat: uall: [x:A]. B[x] not: ¬A set: {x:A| B[x]}  equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B prop: uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  nc-1-as-nc-p fset_wf strong-subtype-self le_wf strong-subtype-set3 strong-subtype-deq-subtype int-deq_wf fset-member_wf not_wf nat_wf dM1_wf nc-e-comp-nc-p
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality setEquality applyEquality because_Cache sqequalRule intEquality independent_isectElimination lambdaEquality natural_numberEquality setElimination rename equalitySymmetry

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i,j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  I\}  ].    ((i1)  =  e(i;j)  \mcdot{}  (j1))



Date html generated: 2016_05_18-PM-00_03_29
Last ObjectModification: 2016_02_05-PM-02_15_28

Theory : cubical!type!theory


Home Index