---

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


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : ℕk
9. dim(b i1) = 1 ∈ ℤ
10. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
11. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
12. i : ℕk
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 ∈ ℤ)
⊢ ∃!b':ℚCube(k). (immediate-rc-face(k;a;b') ∧ immediate-rc-face(k;b';c) ∧ (¬(b' = b ∈ ℚCube(k))))
BY
{ (Assert dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ BY
         (Unfold `rat-cube-dimension` 0
          THEN RepeatFor 2 (AutoSplit)
          THEN (InstLemma `isolate_summand2` [⌜i1⌝]⋅ THENA Auto)
          THEN (RWO "-1" 0 THENA Auto)
          THEN (OReduce 0 THENA Auto)
          THEN (Assert (b i1) = (c i1) ∈ ℚInterval BY
                      Auto)
          THEN (RWW "-1< 9" 0 THENA Auto)
          THEN (Subst' dim(a i1) = 0 ∈ ℤ 0
                THENA (D 11 THEN (RWO "11" 0 THENA Auto) THEN RepUR ``rat-interval-dimension`` 0 THEN AutoSplit)
                )
          THEN (RW IntNormC 0 THENA Auto)
          THEN EqCDA
          THEN AutoSplit)) }

1
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : ℕk
9. dim(b i1) = 1 ∈ ℤ
10. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
11. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
12. i : ℕk
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) ∈ ℤ
⊢ ∃!b':ℚCube(k). (immediate-rc-face(k;a;b') ∧ immediate-rc-face(k;b';c) ∧ (¬(b' = b ∈ ℚCube(k))))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  1  <  dim(c)
6.  immediate-rc-face(k;a;b)
7.  immediate-rc-face(k;b;c)
8.  i1  :  \mBbbN{}k
9.  dim(b  i1)  =  1
10.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i1))  {}\mRightarrow{}  ((a  j)  =  (b  j)))
11.  ((a  i1)  =  [fst((b  i1))])  \mvee{}  ((a  i1)  =  [snd((b  i1))])
12.  i  :  \mBbbN{}k
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)
\mvdash{}  \mexists{}!b':\mBbbQ{}Cube(k).  (immediate-rc-face(k;a;b')  \mwedge{}  immediate-rc-face(k;b';c)  \mwedge{}  (\mneg{}(b'  =  b)))


By

---

Latex:
(Assert  dim(\mlambda{}j.if  (j  =\msubz{}  i1)  then  a  i1  else  c  j  fi  )  =  (dim(c)  -  1)  BY
              (Unfold  `rat-cube-dimension`  0
                THEN  RepeatFor  2  (AutoSplit)
                THEN  (InstLemma  `isolate\_summand2`  [\mkleeneopen{}i1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (RWO  "-1"  0  THENA  Auto)
                THEN  (OReduce  0  THENA  Auto)
                THEN  (Assert  (b  i1)  =  (c  i1)  BY
                                        Auto)
                THEN  (RWW  "-1<  9"  0  THENA  Auto)
                THEN  (Subst'  dim(a  i1)  =  0  0
                            THENA  (D  11
                                          THEN  (RWO  "11"  0  THENA  Auto)
                                          THEN  RepUR  ``rat-interval-dimension``  0
                                          THEN  AutoSplit)
                            )
                THEN  (RW  IntNormC  0  THENA  Auto)
                THEN  EqCDA
                THEN  AutoSplit))

---

Home Index