---

Step * 1 of Lemma cube+_interval-0


1. I : fset(ℕ)
2. i : ℕ
⊢ cube+(I;i) o [0(𝕀)] = <(i0)> ∈ formal-cube(I) j⟶ formal-cube(I+i)
BY
{ (InstLemma `csm-equal` [⌜parm{j}⌝]⋅ THEN (BHyp -1 THENW Auto)) }

1
1. I : fset(ℕ)
2. i : ℕ
3. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
     f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
⊢ cube+(I;i) o [0(𝕀)] = <(i0)> ∈ (I1:fset(ℕ) ⟶ formal-cube(I)(I1) ⟶ formal-cube(I+i)(I1))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
\mvdash{}  cube+(I;i)  o  [0(\mBbbI{})]  =  <(i0)>


By

---

Latex:
(InstLemma  `csm-equal`  [\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}  THEN  (BHyp  -1  THENW  Auto))

---

Home Index