---

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

.....equality..... 
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 ∈ ℤ
17. (f ∈ concat(map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k)))))
⊢ filter(λj.(dim(c j) =z 1);upto(k)) ~ [i]
BY
{ (InstLemma `filter-sq` [⌜ℕk⌝;⌜upto(k)⌝;⌜λj.(dim(c j) =z 1)⌝;⌜λj.(j =z i)⌝]⋅ THENA (Reduce 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,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 ∈ ℤ
17. (f ∈ concat(map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k)))))
18. x : {x:ℕk| (x ∈ upto(k))} 
19. ↑(dim(c x) =z 1)
⊢ x = i ∈ ℤ

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 ∈ ℤ
17. (f ∈ concat(map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k)))))
18. filter(λj.(dim(c j) =z 1);upto(k)) ~ filter(λj.(j =z i);upto(k))
⊢ filter(λj.(dim(c j) =z 1);upto(k)) ~ [i]

---

Latex:

---

Latex:
.....equality..... 
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.  \mforall{}p,q:\mBbbR{}\^{}k.
            ((\mneg{}\mneg{}in-rat-cube(k;p;lower-rc-face(c;i)))  {}\mRightarrow{}  (\mneg{}\mneg{}in-rat-cube(k;q;upper-rc-face(c;i)))  {}\mRightarrow{}  p  \mneq{}  q)
14.  f  :  \mBbbQ{}Cube(k)
15.  f  \mleq{}  c
16.  dim(f)  =  0
17.  (f  \mmember{}  concat(map(\mlambda{}j.[lower-rc-face(c;j);  upper-rc-face(c;j)];
                                        filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k)))))
\mvdash{}  filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k))  \msim{}  [i]


By

---

Latex:
(InstLemma  `filter-sq`  [\mkleeneopen{}\mBbbN{}k\mkleeneclose{};\mkleeneopen{}upto(k)\mkleeneclose{};\mkleeneopen{}\mlambda{}j.(dim(c  j)  =\msubz{}  1)\mkleeneclose{};\mkleeneopen{}\mlambda{}j.(j  =\msubz{}  i)\mkleeneclose{}]\mcdot{}
  THENA  (Reduce  0  THEN  Auto)
  )

---

Home Index