---

Step * 1 1 1 1 of Lemma rat-cube-third-complex


1. k : ℕ
2. n : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K)
5. ∀c,d:ℚCube(k).  ((c ∈ K) ⇒ (d ∈ K) ⇒ Compatible(c;d))
6. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = n ∈ ℤ))
7. c : ℚCube(k)
8. (c ∈ K)
9. p : ℝ^k
10. in-rat-cube(k;p;c)
11. rat-cube-third(k;p;c)
12. j : ℤ
13. d : ℚCube(k)
14. (d ∈ K)
15. ¬rat-cube-third(k;p;d)
16. in-rat-cube(k;p;d)
17. c ⋂ d ≤ c ∧ c ⋂ d ≤ d
18. c ⋂ d = c ∈ ℚCube(k)
⊢ False
BY
{ (InstLemma `rat-cube-face-dimension-equal` [⌜k⌝;⌜d⌝;⌜c⌝]⋅ THEN Auto) }

1
1. k : ℕ
2. n : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K)
5. ∀c,d:ℚCube(k).  ((c ∈ K) ⇒ (d ∈ K) ⇒ Compatible(c;d))
6. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = n ∈ ℤ))
7. c : ℚCube(k)
8. (c ∈ K)
9. p : ℝ^k
10. in-rat-cube(k;p;c)
11. rat-cube-third(k;p;c)
12. j : ℤ
13. d : ℚCube(k)
14. (d ∈ K)
15. ¬rat-cube-third(k;p;d)
16. in-rat-cube(k;p;d)
17. c ⋂ d ≤ c
18. c ⋂ d ≤ d
19. c ⋂ d = c ∈ ℚCube(k)
⊢ ↑Inhabited(d)

2
1. k : ℕ
2. n : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K)
5. ∀c,d:ℚCube(k).  ((c ∈ K) ⇒ (d ∈ K) ⇒ Compatible(c;d))
6. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = n ∈ ℤ))
7. c : ℚCube(k)
8. (c ∈ K)
9. p : ℝ^k
10. in-rat-cube(k;p;c)
11. rat-cube-third(k;p;c)
12. j : ℤ
13. d : ℚCube(k)
14. (d ∈ K)
15. ¬rat-cube-third(k;p;d)
16. in-rat-cube(k;p;d)
17. c ⋂ d ≤ c
18. c ⋂ d ≤ d
19. c ⋂ d = c ∈ ℚCube(k)
⊢ dim(c) = dim(d) ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  \mBbbQ{}Cube(k)  List
4.  no\_repeats(\mBbbQ{}Cube(k);K)
5.  \mforall{}c,d:\mBbbQ{}Cube(k).    ((c  \mmember{}  K)  {}\mRightarrow{}  (d  \mmember{}  K)  {}\mRightarrow{}  Compatible(c;d))
6.  \mforall{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  {}\mRightarrow{}  (dim(c)  =  n))
7.  c  :  \mBbbQ{}Cube(k)
8.  (c  \mmember{}  K)
9.  p  :  \mBbbR{}\^{}k
10.  in-rat-cube(k;p;c)
11.  rat-cube-third(k;p;c)
12.  j  :  \mBbbZ{}
13.  d  :  \mBbbQ{}Cube(k)
14.  (d  \mmember{}  K)
15.  \mneg{}rat-cube-third(k;p;d)
16.  in-rat-cube(k;p;d)
17.  c  \mcap{}  d  \mleq{}  c  \mwedge{}  c  \mcap{}  d  \mleq{}  d
18.  c  \mcap{}  d  =  c
\mvdash{}  False


By

---

Latex:
(InstLemma  `rat-cube-face-dimension-equal`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index