---

Step * 1 1 1 2 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
18. c ⋂ d ≤ d
19. ¬(c ⋂ d = c ∈ ℚCube(k))
20. rat-cube-third(k;p;c)
⊢ ↑Inhabited(c)
BY
{ (BLemma `inhabited-iff-in-rat-cube` THEN Auto) }

---

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
18.  c  \mcap{}  d  \mleq{}  d
19.  \mneg{}(c  \mcap{}  d  =  c)
20.  rat-cube-third(k;p;c)
\mvdash{}  \muparrow{}Inhabited(c)


By

---

Latex:
(BLemma  `inhabited-iff-in-rat-cube`  THEN  Auto)

---

Home Index