---

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

.....assertion..... 
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)
⊢ ||filter(λc@0.is-rat-cube-face(k;c;c@0);(K)')|| = ||filter(λc.is-rat-cube-face(k;a;c);K)|| ∈ ℤ
BY
{ ((BLemma `no_repeats-length-equal-by-relation` THENW Auto)
   THEN Try ((BLemma `no_repeats_filter` THEN Auto THEN GenConclAtAddr [2] THEN D -2 THEN Unhide THEN Auto))
   ) }

1
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∈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))
   ∧ (∀b∈filter(λc.is-rat-cube-face(k;a;c);K).(∃a∈filter(λc@0.is-rat-cube-face(k;c;c@0);(K)'). R a b)))

---

Latex:

---

Latex:
.....assertion..... 
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{}  ||filter(\mlambda{}c@0.is-rat-cube-face(k;c;c@0);(K)')||  =  ||filter(\mlambda{}c.is-rat-cube-face(k;a;c);K)||


By

---

Latex:
((BLemma  `no\_repeats-length-equal-by-relation`  THENW  Auto)
  THEN  Try  ((BLemma  `no\_repeats\_filter`
                        THEN  Auto
                        THEN  GenConclAtAddr  [2]
                        THEN  D  -2
                        THEN  Unhide
                        THEN  Auto))
  )

---

Home Index