---

Step * 2 1 2 1 of Lemma 1-dim-cube-endpoints


1. k : ℕ
2. i : ℕk
⊢ filter(λj.(j =z i);upto(k)) ~ [i]
BY
{ Assert ⌜∀x:ℕ. (filter(λj.(j =z x);upto(k)) ~ if x <z k then [x] else [] fi )⌝⋅ }

1
.....assertion..... 
1. k : ℕ
2. i : ℕk
⊢ ∀x:ℕ. (filter(λj.(j =z x);upto(k)) ~ if x <z k then [x] else [] fi )

2
1. k : ℕ
2. i : ℕk
3. ∀x:ℕ. (filter(λj.(j =z x);upto(k)) ~ if x <z k then [x] else [] fi )
⊢ filter(λj.(j =z i);upto(k)) ~ [i]

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  i  :  \mBbbN{}k
\mvdash{}  filter(\mlambda{}j.(j  =\msubz{}  i);upto(k))  \msim{}  [i]


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x:\mBbbN{}.  (filter(\mlambda{}j.(j  =\msubz{}  x);upto(k))  \msim{}  if  x  <z  k  then  [x]  else  []  fi  )\mkleeneclose{}\mcdot{}

---

Home Index