---

Step * of Lemma face-of-face-pairity

No Annotations
∀k:ℕ. ∀a,b,c:ℚCube(k).
  (1 < dim(c)
  ⇒ immediate-rc-face(k;a;b)
  ⇒ immediate-rc-face(k;b;c)
  ⇒ (∃!b':ℚCube(k). (immediate-rc-face(k;a;b') ∧ immediate-rc-face(k;b';c) ∧ (¬(b' = b ∈ ℚCube(k))))))
BY
{ (Auto
   THEN RepeatFor 2 ((FLemma `immediate-rc-face-implies` [-2] THENA (Auto THEN D -1 THEN Auto)))
   THEN ExRepD
   THEN (Assert dim(a) = (dim(c) - 2) ∈ ℤ BY
               (D 7 THEN D 6 THEN Auto))
   THEN (Assert ↑Inhabited(a) BY
               (RW (AddrC [2] UnfoldTopAbC) (-1) THEN SplitOnHypITE -1  THEN Auto))
   THEN (Assert dim(b) = (dim(c) - 1) ∈ ℤ BY
               (D 7 THEN Auto))
   THEN (Assert ↑Inhabited(b) BY
               (RW (AddrC [2] UnfoldTopAbC) (-1) THEN SplitOnHypITE -1  THEN Auto))
   THEN (Assert ↑Inhabited(c) BY
               (Unfold `rat-cube-dimension` 5 THEN SplitOnHypITE 5  THEN Auto))) }

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)
⊢ ∃!b':ℚCube(k). (immediate-rc-face(k;a;b') ∧ immediate-rc-face(k;b';c) ∧ (¬(b' = b ∈ ℚCube(k))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}a,b,c:\mBbbQ{}Cube(k).
    (1  <  dim(c)
    {}\mRightarrow{}  immediate-rc-face(k;a;b)
    {}\mRightarrow{}  immediate-rc-face(k;b;c)
    {}\mRightarrow{}  (\mexists{}!b':\mBbbQ{}Cube(k).  (immediate-rc-face(k;a;b')  \mwedge{}  immediate-rc-face(k;b';c)  \mwedge{}  (\mneg{}(b'  =  b)))))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((FLemma  `immediate-rc-face-implies`  [-2]  THENA  (Auto  THEN  D  -1  THEN  Auto)))
  THEN  ExRepD
  THEN  (Assert  dim(a)  =  (dim(c)  -  2)  BY
                          (D  7  THEN  D  6  THEN  Auto))
  THEN  (Assert  \muparrow{}Inhabited(a)  BY
                          (RW  (AddrC  [2]  UnfoldTopAbC)  (-1)  THEN  SplitOnHypITE  -1    THEN  Auto))
  THEN  (Assert  dim(b)  =  (dim(c)  -  1)  BY
                          (D  7  THEN  Auto))
  THEN  (Assert  \muparrow{}Inhabited(b)  BY
                          (RW  (AddrC  [2]  UnfoldTopAbC)  (-1)  THEN  SplitOnHypITE  -1    THEN  Auto))
  THEN  (Assert  \muparrow{}Inhabited(c)  BY
                          (Unfold  `rat-cube-dimension`  5  THEN  SplitOnHypITE  5    THEN  Auto)))

---

Home Index