---

Step * 2 2 1 1 1 1 1 1 1 of Lemma rat-complex-boundary-subdiv


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. hlf : ℚCube(k)
6. ↑Inhabited(hlf)
7. dim(hlf) = (n - 1) ∈ ℤ
8. fc : ℚCube(k)
9. ↑in-complex-boundary(k;fc;K)
10. dim(fc) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;hlf;fc)
⊢ (∀a1,a2,b:ℚCube(k).
     (((a1 ∈ (K)') ∧ hlf ≤ a1)
     ⇒ ((a2 ∈ (K)') ∧ hlf ≤ a2)
     ⇒ ((b ∈ K) ∧ fc ≤ b)
     ⇒ (↑is-half-cube(k;a1;b))
     ⇒ (↑is-half-cube(k;a2;b))
     ⇒ (a1 = a2 ∈ ℚCube(k))))
∧ (∀b1,b2,a1:ℚCube(k).
     (((b1 ∈ K) ∧ fc ≤ b1)
     ⇒ ((b2 ∈ K) ∧ fc ≤ b2)
     ⇒ ((a1 ∈ (K)') ∧ hlf ≤ a1)
     ⇒ (↑is-half-cube(k;a1;b1))
     ⇒ (↑is-half-cube(k;a1;b2))
     ⇒ (b1 = b2 ∈ ℚCube(k))))
∧ (∀a1:ℚCube(k). ((a1 ∈ (K)') ⇒ hlf ≤ a1 ⇒ (∃b:ℚCube(k). ((b ∈ K) ∧ fc ≤ b ∧ (↑is-half-cube(k;a1;b))))))
∧ (∀b:ℚCube(k). ((b ∈ K) ⇒ fc ≤ b ⇒ (∃a:ℚCube(k). ((a ∈ (K)') ∧ hlf ≤ a ∧ (↑is-half-cube(k;a;b))))))
BY
{ Auto }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. hlf : ℚCube(k)
6. ↑Inhabited(hlf)
7. dim(hlf) = (n - 1) ∈ ℤ
8. fc : ℚCube(k)
9. ↑in-complex-boundary(k;fc;K)
10. dim(fc) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;hlf;fc)
12. a1 : ℚCube(k)
13. a2 : ℚCube(k)
14. b : ℚCube(k)
15. (a1 ∈ (K)')
16. hlf ≤ a1
17. (a2 ∈ (K)')
18. hlf ≤ a2
19. (b ∈ K)
20. fc ≤ b
21. ↑is-half-cube(k;a1;b)
22. ↑is-half-cube(k;a2;b)
⊢ a1 = a2 ∈ ℚCube(k)

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. hlf : ℚCube(k)
6. ↑Inhabited(hlf)
7. dim(hlf) = (n - 1) ∈ ℤ
8. fc : ℚCube(k)
9. ↑in-complex-boundary(k;fc;K)
10. dim(fc) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;hlf;fc)
12. ∀a1,a2,b:ℚCube(k).
      (((a1 ∈ (K)') ∧ hlf ≤ a1)
      ⇒ ((a2 ∈ (K)') ∧ hlf ≤ a2)
      ⇒ ((b ∈ K) ∧ fc ≤ b)
      ⇒ (↑is-half-cube(k;a1;b))
      ⇒ (↑is-half-cube(k;a2;b))
      ⇒ (a1 = a2 ∈ ℚCube(k)))
13. b1 : ℚCube(k)
14. b2 : ℚCube(k)
15. a1 : ℚCube(k)
16. (b1 ∈ K)
17. fc ≤ b1
18. (b2 ∈ K)
19. fc ≤ b2
20. (a1 ∈ (K)')
21. hlf ≤ a1
22. ↑is-half-cube(k;a1;b1)
23. ↑is-half-cube(k;a1;b2)
⊢ b1 = b2 ∈ ℚCube(k)

3
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. hlf : ℚCube(k)
6. ↑Inhabited(hlf)
7. dim(hlf) = (n - 1) ∈ ℤ
8. fc : ℚCube(k)
9. ↑in-complex-boundary(k;fc;K)
10. dim(fc) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;hlf;fc)
12. ∀a1,a2,b:ℚCube(k).
      (((a1 ∈ (K)') ∧ hlf ≤ a1)
      ⇒ ((a2 ∈ (K)') ∧ hlf ≤ a2)
      ⇒ ((b ∈ K) ∧ fc ≤ b)
      ⇒ (↑is-half-cube(k;a1;b))
      ⇒ (↑is-half-cube(k;a2;b))
      ⇒ (a1 = a2 ∈ ℚCube(k)))
13. ∀b1,b2,a1:ℚCube(k).
      (((b1 ∈ K) ∧ fc ≤ b1)
      ⇒ ((b2 ∈ K) ∧ fc ≤ b2)
      ⇒ ((a1 ∈ (K)') ∧ hlf ≤ a1)
      ⇒ (↑is-half-cube(k;a1;b1))
      ⇒ (↑is-half-cube(k;a1;b2))
      ⇒ (b1 = b2 ∈ ℚCube(k)))
14. a1 : ℚCube(k)
15. (a1 ∈ (K)')
16. hlf ≤ a1
⊢ ∃b:ℚCube(k). ((b ∈ K) ∧ fc ≤ b ∧ (↑is-half-cube(k;a1;b)))

4
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. hlf : ℚCube(k)
6. ↑Inhabited(hlf)
7. dim(hlf) = (n - 1) ∈ ℤ
8. fc : ℚCube(k)
9. ↑in-complex-boundary(k;fc;K)
10. dim(fc) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;hlf;fc)
12. ∀a1,a2,b:ℚCube(k).
      (((a1 ∈ (K)') ∧ hlf ≤ a1)
      ⇒ ((a2 ∈ (K)') ∧ hlf ≤ a2)
      ⇒ ((b ∈ K) ∧ fc ≤ b)
      ⇒ (↑is-half-cube(k;a1;b))
      ⇒ (↑is-half-cube(k;a2;b))
      ⇒ (a1 = a2 ∈ ℚCube(k)))
13. ∀b1,b2,a1:ℚCube(k).
      (((b1 ∈ K) ∧ fc ≤ b1)
      ⇒ ((b2 ∈ K) ∧ fc ≤ b2)
      ⇒ ((a1 ∈ (K)') ∧ hlf ≤ a1)
      ⇒ (↑is-half-cube(k;a1;b1))
      ⇒ (↑is-half-cube(k;a1;b2))
      ⇒ (b1 = b2 ∈ ℚCube(k)))
14. ∀a1:ℚCube(k). ((a1 ∈ (K)') ⇒ hlf ≤ a1 ⇒ (∃b:ℚCube(k). ((b ∈ K) ∧ fc ≤ b ∧ (↑is-half-cube(k;a1;b)))))
15. b : ℚCube(k)
16. (b ∈ K)
17. fc ≤ b
⊢ ∃a:ℚCube(k). ((a ∈ (K)') ∧ hlf ≤ a ∧ (↑is-half-cube(k;a;b)))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  \mneg{}(n  =  0)
5.  hlf  :  \mBbbQ{}Cube(k)
6.  \muparrow{}Inhabited(hlf)
7.  dim(hlf)  =  (n  -  1)
8.  fc  :  \mBbbQ{}Cube(k)
9.  \muparrow{}in-complex-boundary(k;fc;K)
10.  dim(fc)  =  (n  -  1)
11.  \muparrow{}is-half-cube(k;hlf;fc)
\mvdash{}  (\mforall{}a1,a2,b:\mBbbQ{}Cube(k).
          (((a1  \mmember{}  (K)')  \mwedge{}  hlf  \mleq{}  a1)
          {}\mRightarrow{}  ((a2  \mmember{}  (K)')  \mwedge{}  hlf  \mleq{}  a2)
          {}\mRightarrow{}  ((b  \mmember{}  K)  \mwedge{}  fc  \mleq{}  b)
          {}\mRightarrow{}  (\muparrow{}is-half-cube(k;a1;b))
          {}\mRightarrow{}  (\muparrow{}is-half-cube(k;a2;b))
          {}\mRightarrow{}  (a1  =  a2)))
\mwedge{}  (\mforall{}b1,b2,a1:\mBbbQ{}Cube(k).
          (((b1  \mmember{}  K)  \mwedge{}  fc  \mleq{}  b1)
          {}\mRightarrow{}  ((b2  \mmember{}  K)  \mwedge{}  fc  \mleq{}  b2)
          {}\mRightarrow{}  ((a1  \mmember{}  (K)')  \mwedge{}  hlf  \mleq{}  a1)
          {}\mRightarrow{}  (\muparrow{}is-half-cube(k;a1;b1))
          {}\mRightarrow{}  (\muparrow{}is-half-cube(k;a1;b2))
          {}\mRightarrow{}  (b1  =  b2)))
\mwedge{}  (\mforall{}a1:\mBbbQ{}Cube(k)
          ((a1  \mmember{}  (K)')  {}\mRightarrow{}  hlf  \mleq{}  a1  {}\mRightarrow{}  (\mexists{}b:\mBbbQ{}Cube(k).  ((b  \mmember{}  K)  \mwedge{}  fc  \mleq{}  b  \mwedge{}  (\muparrow{}is-half-cube(k;a1;b))))))
\mwedge{}  (\mforall{}b:\mBbbQ{}Cube(k)
          ((b  \mmember{}  K)  {}\mRightarrow{}  fc  \mleq{}  b  {}\mRightarrow{}  (\mexists{}a:\mBbbQ{}Cube(k).  ((a  \mmember{}  (K)')  \mwedge{}  hlf  \mleq{}  a  \mwedge{}  (\muparrow{}is-half-cube(k;a;b))))))


By

---

Latex:
Auto

---

Home Index