---

Step * of Lemma 1-dim-cube-endpoints

∀k:ℕ. ∀c:ℚCube(k).
  ((dim(c) = 1 ∈ ℤ)
  ⇒ (∃a,b:ℚCube(k)
       (a ≤ c
       ∧ b ≤ c
       ∧ (dim(a) = 0 ∈ ℤ)
       ∧ (dim(b) = 0 ∈ ℤ)
       ∧ (∀p,q:ℝ^k.  ((¬¬in-rat-cube(k;p;a)) ⇒ (¬¬in-rat-cube(k;q;b)) ⇒ p ≠ q))
       ∧ (∀f:ℚCube(k). (f ≤ c ⇒ (dim(f) = 0 ∈ ℤ) ⇒ ((f = a ∈ ℚCube(k)) ∨ (f = b ∈ ℚCube(k))))))))
BY
{ ((Auto THEN (Assert ↑Inhabited(c) BY (Unfold `rat-cube-dimension` -1 THEN SplitOnHypITE -1  THEN Auto)))
   THEN DupHyp (-2)
   THEN (RWO "rat-cube-dimension-1" (-1) THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜lower-rc-face(c;i)⌝;⌜upper-rc-face(c;i)⌝]⋅
   THEN Auto
   THEN RWW "lower-rc-face-dimension upper-rc-face-dimension" 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. ¬¬in-rat-cube(k;p;lower-rc-face(c;i))
16. ¬¬in-rat-cube(k;q;upper-rc-face(c;i))
⊢ p ≠ q

2
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,q:ℝ^k.  ((¬¬in-rat-cube(k;p;lower-rc-face(c;i))) ⇒ (¬¬in-rat-cube(k;q;upper-rc-face(c;i))) ⇒ p ≠ q)
14. f : ℚCube(k)
15. f ≤ c
16. dim(f) = 0 ∈ ℤ
⊢ (f = lower-rc-face(c;i) ∈ ℚCube(k)) ∨ (f = upper-rc-face(c;i) ∈ ℚCube(k))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).
    ((dim(c)  =  1)
    {}\mRightarrow{}  (\mexists{}a,b:\mBbbQ{}Cube(k)
              (a  \mleq{}  c
              \mwedge{}  b  \mleq{}  c
              \mwedge{}  (dim(a)  =  0)
              \mwedge{}  (dim(b)  =  0)
              \mwedge{}  (\mforall{}p,q:\mBbbR{}\^{}k.    ((\mneg{}\mneg{}in-rat-cube(k;p;a))  {}\mRightarrow{}  (\mneg{}\mneg{}in-rat-cube(k;q;b))  {}\mRightarrow{}  p  \mneq{}  q))
              \mwedge{}  (\mforall{}f:\mBbbQ{}Cube(k).  (f  \mleq{}  c  {}\mRightarrow{}  (dim(f)  =  0)  {}\mRightarrow{}  ((f  =  a)  \mvee{}  (f  =  b)))))))


By

---

Latex:
((Auto
    THEN  (Assert  \muparrow{}Inhabited(c)  BY
                            (Unfold  `rat-cube-dimension`  -1  THEN  SplitOnHypITE  -1    THEN  Auto))
    )
  THEN  DupHyp  (-2)
  THEN  (RWO  "rat-cube-dimension-1"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}lower-rc-face(c;i)\mkleeneclose{};\mkleeneopen{}upper-rc-face(c;i)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWW  "lower-rc-face-dimension  upper-rc-face-dimension"  0
  THEN  Auto)

---

Home Index