---

Step * 1 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) ∈ ℤ
18. Compatible(c1;c2)
⊢ Compatible(c;d)
BY
{ (InstLemma `faces-of-compatible-rat-cubes` [⌜k⌝;⌜c⌝;⌜d⌝;⌜c2⌝;⌜c1⌝]⋅ THEN Auto) }

1
.....antecedent..... 
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(c2;c1)

---

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)
18.  Compatible(c1;c2)
\mvdash{}  Compatible(c;d)


By

---

Latex:
(InstLemma  `faces-of-compatible-rat-cubes`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index