---

Step * of Lemma member-rat-complex-boundary-n

∀n,k:ℕ. ∀K:n-dim-complex. ∀f:ℚCube(k).  ((f ∈ ∂(K)) ⇐⇒ (↑in-complex-boundary(k;f;K)) ∧ (dim(f) = (n - 1) ∈ ℤ))
BY
{ ((UnivCD THENA Auto)
   THEN DVar `K'
   THEN (Assert face-complex(k;K) ∈ ℚCube(k) List BY
               ProveWfLemma)
   THEN RepUR ``rat-complex-boundary rat-cube-sub-complex`` 0
   THEN (RWO "member_filter" 0 THENA Auto)
   THEN (Reduce 0 THEN (RWO "member-face-complex" 0 THENA Auto))
   THEN RWO "member-rat-cube-faces" 0
   THEN Auto) }

1
1. n : ℕ
2. k : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K)
5. (∀c,d∈K.  Compatible(c;d))
6. (∀c∈K.dim(c) = n ∈ ℤ)
7. f : ℚCube(k)
8. face-complex(k;K) ∈ ℚCube(k) List
9. ∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))
10. ↑in-complex-boundary(k;f;K)
⊢ dim(f) = (n - 1) ∈ ℤ

2
1. n : ℕ
2. k : ℕ
3. K : ℚCube(k) List
4. [%1] : no_repeats(ℚCube(k);K) ∧ (∀c,d∈K.  Compatible(c;d)) ∧ (∀c∈K.dim(c) = n ∈ ℤ)
5. f : ℚCube(k)
6. face-complex(k;K) ∈ ℚCube(k) List
7. ↑in-complex-boundary(k;f;K)
8. dim(f) = (n - 1) ∈ ℤ
⊢ ∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}n,k:\mBbbN{}.  \mforall{}K:n-dim-complex.  \mforall{}f:\mBbbQ{}Cube(k).
    ((f  \mmember{}  \mpartial{}(K))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}in-complex-boundary(k;f;K))  \mwedge{}  (dim(f)  =  (n  -  1)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  DVar  `K'
  THEN  (Assert  face-complex(k;K)  \mmember{}  \mBbbQ{}Cube(k)  List  BY
                          ProveWfLemma)
  THEN  RepUR  ``rat-complex-boundary  rat-cube-sub-complex``  0
  THEN  (RWO  "member\_filter"  0  THENA  Auto)
  THEN  (Reduce  0  THEN  (RWO  "member-face-complex"  0  THENA  Auto))
  THEN  RWO  "member-rat-cube-faces"  0
  THEN  Auto)

---

Home Index