---

Step * 1 of Lemma 1-dim-cube-endpoints


1. k : ℕ
2. c : ℚCube(k)
3. dim(c) = 1 ∈ ℤ
4. ↑Inhabited(c)
5. ↑Inhabited(c)
6. i : ℕk
7. dim(c i) = 1 ∈ ℤ
8. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ (dim(c j) = 0 ∈ ℤ))
9. lower-rc-face(c;i) ≤ c
10. upper-rc-face(c;i) ≤ c
11. dim(lower-rc-face(c;i)) = 0 ∈ ℤ
12. dim(upper-rc-face(c;i)) = 0 ∈ ℤ
13. p : ℝ^k
14. q : ℝ^k
15. ¬¬in-rat-cube(k;p;lower-rc-face(c;i))
16. ¬¬in-rat-cube(k;q;upper-rc-face(c;i))
⊢ p ≠ q
BY
{ ((RWO "not-not-in-0-dim-cube" (-2) THEN Auto)
   THEN RWO "not-not-in-0-dim-cube" (-1)
   THEN Auto
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN (RWO "real-vec-sep-iff-rneq" 0 THEN Auto)
   THEN Reduce 0
   THEN D 0 With ⌜i⌝ 
   THEN Auto
   THEN RWO "rneq-rat2real" 0
   THEN Auto) }

1
1. k : ℕ
2. c : ℚCube(k)
3. dim(c) = 1 ∈ ℤ
4. ↑Inhabited(c)
5. ↑Inhabited(c)
6. i : ℕk
7. dim(c i) = 1 ∈ ℤ
8. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ (dim(c j) = 0 ∈ ℤ))
9. lower-rc-face(c;i) ≤ c
10. upper-rc-face(c;i) ≤ c
11. dim(lower-rc-face(c;i)) = 0 ∈ ℤ
12. dim(upper-rc-face(c;i)) = 0 ∈ ℤ
13. p : ℝ^k
14. q : ℝ^k
15. req-vec(k;p;λj.rat2real(fst((lower-rc-face(c;i) j))))
16. req-vec(k;q;λj.rat2real(fst((upper-rc-face(c;i) j))))
⊢ ¬((fst((lower-rc-face(c;i) i))) = (fst((upper-rc-face(c;i) i))) ∈ ℚ)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  dim(c)  =  1
4.  \muparrow{}Inhabited(c)
5.  \muparrow{}Inhabited(c)
6.  i  :  \mBbbN{}k
7.  dim(c  i)  =  1
8.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  (dim(c  j)  =  0))
9.  lower-rc-face(c;i)  \mleq{}  c
10.  upper-rc-face(c;i)  \mleq{}  c
11.  dim(lower-rc-face(c;i))  =  0
12.  dim(upper-rc-face(c;i))  =  0
13.  p  :  \mBbbR{}\^{}k
14.  q  :  \mBbbR{}\^{}k
15.  \mneg{}\mneg{}in-rat-cube(k;p;lower-rc-face(c;i))
16.  \mneg{}\mneg{}in-rat-cube(k;q;upper-rc-face(c;i))
\mvdash{}  p  \mneq{}  q


By

---

Latex:
((RWO  "not-not-in-0-dim-cube"  (-2)  THEN  Auto)
  THEN  RWO  "not-not-in-0-dim-cube"  (-1)
  THEN  Auto
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  (RWO  "real-vec-sep-iff-rneq"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
  THEN  Auto
  THEN  RWO  "rneq-rat2real"  0
  THEN  Auto)

---

Home Index