---

Step * 1 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 ≤ 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)
BY
{ (Assert Compatible(c1;c2) BY
         (DVar `K' THEN Unhide THEN Auto THEN RWO  "pairwise-iff" 5 THEN EAuto 1)) }

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) ∈ ℤ
18. Compatible(c1;c2)
⊢ 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  \mleq{}  c2
12.  dim(c)  =  (dim(c2)  -  1)
13.  c1  :  \mBbbQ{}Cube(k)
14.  (c1  \mmember{}  K)
15.  \muparrow{}Inhabited(c1)
16.  d  \mleq{}  c1
17.  dim(d)  =  (dim(c1)  -  1)
\mvdash{}  Compatible(c;d)


By

---

Latex:
(Assert  Compatible(c1;c2)  BY
              (DVar  `K'  THEN  Unhide  THEN  Auto  THEN  RWO    "pairwise-iff"  5  THEN  EAuto  1))

---

Home Index