---

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


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. c : ℚCube(k)
6. ↑Inhabited(c)
7. dim(c) = (n - 1) ∈ ℤ
8. a : ℚCube(k)
9. ↑in-complex-boundary(k;a;K)
10. dim(a) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;c;a)
⊢ ∃R:ℚCube(k) ⟶ ℚCube(k) ⟶ ℙ
   ((∀a1,a2,b:ℚCube(k).
       ((a1 ∈ filter(λc@0.is-rat-cube-face(k;c;c@0);(K)'))
       ⇒ (a2 ∈ filter(λc@0.is-rat-cube-face(k;c;c@0);(K)'))
       ⇒ (b ∈ filter(λc.is-rat-cube-face(k;a;c);K))
       ⇒ (R a1 b)
       ⇒ (R a2 b)
       ⇒ (a1 = a2 ∈ ℚCube(k))))
   ∧ (∀b1,b2,a1:ℚCube(k).
        ((b1 ∈ filter(λc.is-rat-cube-face(k;a;c);K))
        ⇒ (b2 ∈ filter(λc.is-rat-cube-face(k;a;c);K))
        ⇒ (a1 ∈ filter(λc@0.is-rat-cube-face(k;c;c@0);(K)'))
        ⇒ (R a1 b1)
        ⇒ (R a1 b2)
        ⇒ (b1 = b2 ∈ ℚCube(k))))
   ∧ (∀a1:ℚCube(k)
        ((a1 ∈ (K)')
        ⇒ (↑is-rat-cube-face(k;c;a1))
        ⇒ (∃b:ℚCube(k). ((b ∈ K) ∧ (↑is-rat-cube-face(k;a;b)) ∧ (R a1 b)))))
   ∧ (∀b:ℚCube(k)
        ((b ∈ K) ⇒ (↑is-rat-cube-face(k;a;b)) ⇒ (∃a:ℚCube(k). ((a ∈ (K)') ∧ (↑is-rat-cube-face(k;c;a)) ∧ (R a b))))))
BY
{ (RenameVar `fc' (-4) THEN RenameVar `hlf' 5) }

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)
⊢ ∃R:ℚCube(k) ⟶ ℚCube(k) ⟶ ℙ
   ((∀a1,a2,b:ℚCube(k).
       ((a1 ∈ filter(λc@0.is-rat-cube-face(k;hlf;c@0);(K)'))
       ⇒ (a2 ∈ filter(λc@0.is-rat-cube-face(k;hlf;c@0);(K)'))
       ⇒ (b ∈ filter(λc.is-rat-cube-face(k;fc;c);K))
       ⇒ (R a1 b)
       ⇒ (R a2 b)
       ⇒ (a1 = a2 ∈ ℚCube(k))))
   ∧ (∀b1,b2,a1:ℚCube(k).
        ((b1 ∈ filter(λc.is-rat-cube-face(k;fc;c);K))
        ⇒ (b2 ∈ filter(λc.is-rat-cube-face(k;fc;c);K))
        ⇒ (a1 ∈ filter(λc@0.is-rat-cube-face(k;hlf;c@0);(K)'))
        ⇒ (R a1 b1)
        ⇒ (R a1 b2)
        ⇒ (b1 = b2 ∈ ℚCube(k))))
   ∧ (∀a1:ℚCube(k)
        ((a1 ∈ (K)')
        ⇒ (↑is-rat-cube-face(k;hlf;a1))
        ⇒ (∃b:ℚCube(k). ((b ∈ K) ∧ (↑is-rat-cube-face(k;fc;b)) ∧ (R a1 b)))))
   ∧ (∀b:ℚCube(k)
        ((b ∈ K)
        ⇒ (↑is-rat-cube-face(k;fc;b))
        ⇒ (∃a:ℚCube(k). ((a ∈ (K)') ∧ (↑is-rat-cube-face(k;hlf;a)) ∧ (R a b))))))

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `fc'  (-4)  THEN  RenameVar  `hlf'  5)

---

Home Index