---

Step * of Lemma member-rat-complex-boundary

∀k:ℕ. ∀K:ℚCube(k) List. ∀f:ℚCube(k).
  ((f ∈ ∂(K))
  ⇐⇒ (∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))) ∧ (↑in-complex-boundary(k;f;K)))
BY
{ ((UnivCD THENA Auto)
   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) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  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