---

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


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]
BY
{ (RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  i  :  \mBbbN{}k
3.  \mforall{}x:\mBbbN{}.  (filter(\mlambda{}j.(j  =\msubz{}  x);upto(k))  \msim{}  if  x  <z  k  then  [x]  else  []  fi  )
\mvdash{}  filter(\mlambda{}j.(j  =\msubz{}  i);upto(k))  \msim{}  [i]


By

---

Latex:
(RWO    "-1"  0  THEN  Auto)

---

Home Index