---

Step * 1 1 1 4 1 1 2 1 2 of Lemma face-of-face-pairity


1. k : ℕ
2. i1 : ℕk
3. i : ℕk
4. a : ℚCube(k)
5. b : ℚCube(k)
6. c : ℚCube(k)
7. 1 < dim(c)
8. immediate-rc-face(k;a;b)
9. immediate-rc-face(k;b;c)
10. dim(b i1) = 1 ∈ ℤ
11. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
12. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi  ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. i3 : ℕk
33. dim(y i1) = 1 ∈ ℤ
34. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval))
35. ((a i1) = [fst((y i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((y i1))] ∈ ℚInterval)
36. i2 : ℕk
37. dim(c i) = 1 ∈ ℤ
38. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval))
39. ((y i) = [fst((c i))] ∈ ℚInterval) ∨ ((y i) = [snd((c i))] ∈ ℚInterval)
40. ¬(i = i1 ∈ ℤ)
41. y = b ∈ ℚCube(k)
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
BY
{ Auto }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  i1  :  \mBbbN{}k
3.  i  :  \mBbbN{}k
4.  a  :  \mBbbQ{}Cube(k)
5.  b  :  \mBbbQ{}Cube(k)
6.  c  :  \mBbbQ{}Cube(k)
7.  1  <  dim(c)
8.  immediate-rc-face(k;a;b)
9.  immediate-rc-face(k;b;c)
10.  dim(b  i1)  =  1
11.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i1))  {}\mRightarrow{}  ((a  j)  =  (b  j)))
12.  ((a  i1)  =  [fst((b  i1))])  \mvee{}  ((a  i1)  =  [snd((b  i1))])
13.  dim(c  i)  =  1
14.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((b  j)  =  (c  j)))
15.  ((b  i)  =  [fst((c  i))])  \mvee{}  ((b  i)  =  [snd((c  i))])
16.  dim(a)  =  (dim(c)  -  2)
17.  \muparrow{}Inhabited(a)
18.  dim(b)  =  (dim(c)  -  1)
19.  \muparrow{}Inhabited(b)
20.  \muparrow{}Inhabited(c)
21.  \mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi    \mmember{}  \mBbbQ{}Cube(k)
22.  \muparrow{}Inhabited(\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )
23.  \mneg{}(i1  =  i)
24.  dim(\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )  =  (dim(c)  -  1)
25.  immediate-rc-face(k;a;\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )
26.  immediate-rc-face(k;\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  ;c)
27.  \mneg{}((\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )  =  b)
28.  y  :  \mBbbQ{}Cube(k)
29.  immediate-rc-face(k;a;y)
30.  immediate-rc-face(k;y;c)
31.  \mneg{}(y  =  b)
32.  i3  :  \mBbbN{}k
33.  dim(y  i1)  =  1
34.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i1))  {}\mRightarrow{}  ((a  j)  =  (y  j)))
35.  ((a  i1)  =  [fst((y  i1))])  \mvee{}  ((a  i1)  =  [snd((y  i1))])
36.  i2  :  \mBbbN{}k
37.  dim(c  i)  =  1
38.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((y  j)  =  (c  j)))
39.  ((y  i)  =  [fst((c  i))])  \mvee{}  ((y  i)  =  [snd((c  i))])
40.  \mneg{}(i  =  i1)
41.  y  =  b
\mvdash{}  y  =  (\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )


By

---

Latex:
Auto

---

Home Index