---

Step * of Lemma rat-complex-boundary-remove1

∀k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k).
  ((c ∈ K)
  ⇒ (∀f:ℚCube(k)
        ((f ∈ ∂(rat-cube-sub-complex(λa.(¬brceq(k;a;c));K)))
        ⇐⇒ ((f ∈ ∂(K)) ∧ (¬f ≤ c)) ∨ ((¬(f ∈ ∂(K))) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)))))
BY
{ (Auto
   THEN (All (RWO  "member-rat-complex-boundary") THENA Auto)
   THEN ExRepD
   THEN SplitOrHyps
   THEN ExRepD
   THEN ((Unfold `rat-cube-sub-complex` 0
          THEN (RWO "member_filter" 0 THENA Auto)
          THEN Reduce 0
          THEN (RW assert_pushdownC 0 THENA Auto)
          THEN (RWO "assert-rceq" 0 THENA Auto))
   ORELSE (Unfold `rat-cube-sub-complex` 8
           THEN (RWO "member_filter" 8 THENA Auto)
           THEN Reduce 8
           THEN (RW assert_pushdownC 8 THENA Auto)
           THEN (RWO "assert-rceq" 8 THENA Auto))
   )) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. c : ℚCube(k)
5. (c ∈ K)
6. f : ℚCube(k)
7. c1 : ℚCube(k)
8. (c1 ∈ K) ∧ (¬(c1 = c ∈ ℚCube(k)))
9. ↑Inhabited(c1)
10. f ≤ c1
11. dim(f) = (dim(c1) - 1) ∈ ℤ
12. ↑in-complex-boundary(k;f;rat-cube-sub-complex(λa.(¬brceq(k;a;c));K))
⊢ (((∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))) ∧ (↑in-complex-boundary(k;f;K)))
∧ (¬f ≤ c))
∨ ((¬((∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))) ∧ (↑in-complex-boundary(k;f;K))))
  ∧ f ≤ c
  ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. c : ℚCube(k)
5. (c ∈ K)
6. f : ℚCube(k)
7. c1 : ℚCube(k)
8. (c1 ∈ K)
9. ↑Inhabited(c1)
10. f ≤ c1
11. dim(f) = (dim(c1) - 1) ∈ ℤ
12. ↑in-complex-boundary(k;f;K)
13. ¬f ≤ c
⊢ (∃c1:ℚCube(k). (((c1 ∈ K) ∧ (¬(c1 = c ∈ ℚCube(k)))) ∧ (↑Inhabited(c1)) ∧ f ≤ c1 ∧ (dim(f) = (dim(c1) - 1) ∈ ℤ)))
∧ (↑in-complex-boundary(k;f;filter(λa.(¬brceq(k;a;c));K)))

3
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. c : ℚCube(k)
5. (c ∈ K)
6. f : ℚCube(k)
7. ¬((∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))) ∧ (↑in-complex-boundary(k;f;K)))
8. f ≤ c
9. dim(f) = (dim(c) - 1) ∈ ℤ
⊢ (∃c1:ℚCube(k). (((c1 ∈ K) ∧ (¬(c1 = c ∈ ℚCube(k)))) ∧ (↑Inhabited(c1)) ∧ f ≤ c1 ∧ (dim(f) = (dim(c1) - 1) ∈ ℤ)))
∧ (↑in-complex-boundary(k;f;filter(λa.(¬brceq(k;a;c));K)))

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.  \mforall{}K:n-dim-complex.  \mforall{}c:\mBbbQ{}Cube(k).
    ((c  \mmember{}  K)
    {}\mRightarrow{}  (\mforall{}f:\mBbbQ{}Cube(k)
                ((f  \mmember{}  \mpartial{}(rat-cube-sub-complex(\mlambda{}a.(\mneg{}\msubb{}rceq(k;a;c));K)))
                \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  \mpartial{}(K))  \mwedge{}  (\mneg{}f  \mleq{}  c))  \mvee{}  ((\mneg{}(f  \mmember{}  \mpartial{}(K)))  \mwedge{}  f  \mleq{}  c  \mwedge{}  (dim(f)  =  (dim(c)  -  1))))))


By

---

Latex:
(Auto
  THEN  (All  (RWO    "member-rat-complex-boundary")  THENA  Auto)
  THEN  ExRepD
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  ((Unfold  `rat-cube-sub-complex`  0
                THEN  (RWO  "member\_filter"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (RW  assert\_pushdownC  0  THENA  Auto)
                THEN  (RWO  "assert-rceq"  0  THENA  Auto))
  ORELSE  (Unfold  `rat-cube-sub-complex`  8
                  THEN  (RWO  "member\_filter"  8  THENA  Auto)
                  THEN  Reduce  8
                  THEN  (RW  assert\_pushdownC  8  THENA  Auto)
                  THEN  (RWO  "assert-rceq"  8  THENA  Auto))
  ))

---

Home Index