---

Step * of Lemma face-complex_wf

∀[k:ℕ]. ∀[n:ℕ+]. ∀[K:n-dim-complex].  (face-complex(k;K) ∈ n - 1-dim-complex)
BY
{ (Auto
   THEN (Assert face-complex(k;K) ∈ ℚCube(k) List BY
               ProveWfLemma)
   THEN MemTypeCD
   THEN Auto
   THEN RWO "l_all_iff pairwise-iff" 0
   THEN Auto
   THEN EAuto 1
   THEN (All (RWO "member-face-complex") THENA Auto)
   THEN ExRepD) }

1
1. k : ℕ
2. n : ℕ+
3. K : n-dim-complex
4. face-complex(k;K) ∈ ℚCube(k) List
5. no_repeats(ℚCube(k);face-complex(k;K))
6. c : ℚCube(k)
7. d : ℚCube(k)
8. c2 : ℚCube(k)
9. (c2 ∈ K)
10. ↑Inhabited(c2)
11. (c ∈ rat-cube-faces(k;c2))
12. c1 : ℚCube(k)
13. (c1 ∈ K)
14. ↑Inhabited(c1)
15. (d ∈ rat-cube-faces(k;c1))
⊢ Compatible(c;d)

2
1. k : ℕ
2. n : ℕ+
3. K : n-dim-complex
4. face-complex(k;K) ∈ ℚCube(k) List
5. no_repeats(ℚCube(k);face-complex(k;K))
6. (∀c,d∈face-complex(k;K).  Compatible(c;d))
7. c : ℚCube(k)
8. c1 : ℚCube(k)
9. (c1 ∈ K)
10. ↑Inhabited(c1)
11. (c ∈ rat-cube-faces(k;c1))
⊢ dim(c) = (n - 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[K:n-dim-complex].    (face-complex(k;K)  \mmember{}  n  -  1-dim-complex)


By

---

Latex:
(Auto
  THEN  (Assert  face-complex(k;K)  \mmember{}  \mBbbQ{}Cube(k)  List  BY
                          ProveWfLemma)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWO  "l\_all\_iff  pairwise-iff"  0
  THEN  Auto
  THEN  EAuto  1
  THEN  (All  (RWO  "member-face-complex")  THENA  Auto)
  THEN  ExRepD)

---

Home Index