---

Step * 1 of Lemma face-complex_wf


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)
BY
{ (All (RWO  "member-rat-cube-faces") THEN Auto) }

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 ≤ c2
12. dim(c) = (dim(c2) - 1) ∈ ℤ
13. c1 : ℚCube(k)
14. (c1 ∈ K)
15. ↑Inhabited(c1)
16. d ≤ c1
17. dim(d) = (dim(c1) - 1) ∈ ℤ
⊢ Compatible(c;d)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  K  :  n-dim-complex
4.  face-complex(k;K)  \mmember{}  \mBbbQ{}Cube(k)  List
5.  no\_repeats(\mBbbQ{}Cube(k);face-complex(k;K))
6.  c  :  \mBbbQ{}Cube(k)
7.  d  :  \mBbbQ{}Cube(k)
8.  c2  :  \mBbbQ{}Cube(k)
9.  (c2  \mmember{}  K)
10.  \muparrow{}Inhabited(c2)
11.  (c  \mmember{}  rat-cube-faces(k;c2))
12.  c1  :  \mBbbQ{}Cube(k)
13.  (c1  \mmember{}  K)
14.  \muparrow{}Inhabited(c1)
15.  (d  \mmember{}  rat-cube-faces(k;c1))
\mvdash{}  Compatible(c;d)


By

---

Latex:
(All  (RWO    "member-rat-cube-faces")  THEN  Auto)

---

Home Index