---

Step * 1 1 of Lemma has-interior-point-implies


1. k : ℕ
2. c : ℚCube(k)
3. a : ℚCube(k)
4. x : ℕk ⟶ ℚ
5. rat-point-in-cube(k;x;c)
6. rat-point-in-cube-interior(k;x;a)
7. dim(c) < dim(a)
8. d : ℚCube(k)
9. ↑is-half-cube(k;c;d)
10. d ≤ a
11. rat-point-in-cube(k;x;d)
12. d = a ∈ ℚCube(k)
⊢ False
BY
{ ((FLemma `half-cube-dimension` [-4] THENM RWO "-2" (-1)) THEN Auto) }

1
.....wf..... 
1. k : ℕ
2. c : ℚCube(k)
3. a : ℚCube(k)
4. x : ℕk ⟶ ℚ
5. rat-point-in-cube(k;x;c)
6. rat-point-in-cube-interior(k;x;a)
7. dim(c) < dim(a)
8. d : ℚCube(k)
9. ↑is-half-cube(k;c;d)
10. d ≤ a
11. rat-point-in-cube(k;x;d)
12. d = a ∈ ℚCube(k)
⊢ d ∈ {c:ℚCube(k)| ↑Inhabited(c)} 

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  a  :  \mBbbQ{}Cube(k)
4.  x  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
5.  rat-point-in-cube(k;x;c)
6.  rat-point-in-cube-interior(k;x;a)
7.  dim(c)  <  dim(a)
8.  d  :  \mBbbQ{}Cube(k)
9.  \muparrow{}is-half-cube(k;c;d)
10.  d  \mleq{}  a
11.  rat-point-in-cube(k;x;d)
12.  d  =  a
\mvdash{}  False


By

---

Latex:
((FLemma  `half-cube-dimension`  [-4]  THENM  RWO  "-2"  (-1))  THEN  Auto)

---

Home Index