---

Step * 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
⊢ False
BY
{ (Decide ⌜c ⋂ d = c ∈ ℚCube(k)⌝⋅ THENA 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 ∧ c ⋂ d ≤ d
18. c ⋂ d = c ∈ ℚCube(k)
⊢ False

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 ∧ c ⋂ d ≤ d
18. ¬(c ⋂ d = c ∈ ℚCube(k))
⊢ False

---

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
\mvdash{}  False


By

---

Latex:
(Decide  \mkleeneopen{}c  \mcap{}  d  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index