Nuprl Lemma : nc-s-i1-j1

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


Proof




Definitions occuring in Statement :  nc-1: (i1) nc-s: s 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 squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q so_lambda: λ2x.t[x] nat: so_apply: x[s] all: x:A. B[x]
Lemmas referenced :  nc-1_wf add-name_wf equal_wf squash_wf true_wf names-hom_wf fset_wf nat_wf add-name-com iff_weakening_equal set_wf not_wf fset-member_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf strong-subtype-self nh-comp-assoc nc-s_wf f-subset-add-name nh-comp_wf nc-1-s-commute nh-id-left s-comp-nc-1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis applyEquality instantiate lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination hyp_replacement intEquality isect_memberEquality axiomEquality dependent_functionElimination

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



Date html generated: 2017_10_05-AM-01_06_41
Last ObjectModification: 2017_07_28-AM-09_28_00

Theory : cubical!type!theory


Home Index