---

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


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. c : ℚCube(k)
5. (c ∈ K)
6. p : ℝ^k
7. in-rat-cube(k;p;c)
8. rat-cube-third(k;p;c)
9. j : ℤ
10. d : ℚCube(k)
11. (d ∈ K)
12. ¬rat-cube-third(k;p;d)
13. in-rat-cube(k;p;d)
⊢ False
BY
{ (DVar `K'
   THEN Auto
   THEN (RWO "pairwise-iff" 5 THENA EAuto 1)
   THEN (RWO "l_all_iff" 6 THENA Auto)
   THEN (Assert Compatible(c;d) BY
               Auto)
   THEN (D -1 THENA ((BLemma `inhabited-iff-in-rat-cube` THENM D 0 With ⌜p⌝ ) THEN EAuto 1))) }

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
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  c  :  \mBbbQ{}Cube(k)
5.  (c  \mmember{}  K)
6.  p  :  \mBbbR{}\^{}k
7.  in-rat-cube(k;p;c)
8.  rat-cube-third(k;p;c)
9.  j  :  \mBbbZ{}
10.  d  :  \mBbbQ{}Cube(k)
11.  (d  \mmember{}  K)
12.  \mneg{}rat-cube-third(k;p;d)
13.  in-rat-cube(k;p;d)
\mvdash{}  False


By

---

Latex:
(DVar  `K'
  THEN  Auto
  THEN  (RWO  "pairwise-iff"  5  THENA  EAuto  1)
  THEN  (RWO  "l\_all\_iff"  6  THENA  Auto)
  THEN  (Assert  Compatible(c;d)  BY
                          Auto)
  THEN  (D  -1  THENA  ((BLemma  `inhabited-iff-in-rat-cube`  THENM  D  0  With  \mkleeneopen{}p\mkleeneclose{}  )  THEN  EAuto  1)))

---

Home Index