---

Step * of Lemma equal-rat-cube-complexes

∀k:ℕ
  ∀[n:ℕ]
    ∀K,L:n-dim-complex.
      uiff(permutation(ℚCube(k);K;L);∀c:{c:ℚCube(k)| (↑Inhabited(c)) ∧ (dim(c) = n ∈ ℤ)} . ((c ∈ K) ⇐⇒ (c ∈ L)))
BY
{ Auto }

1
1. k : ℕ
2. [n] : ℕ
3. K : n-dim-complex
4. L : n-dim-complex
5. [%] : permutation(ℚCube(k);K;L)
6. c : {c:ℚCube(k)| (↑Inhabited(c)) ∧ (dim(c) = n ∈ ℤ)} 
7. (c ∈ K)
⊢ (c ∈ L)

2
1. k : ℕ
2. [n] : ℕ
3. K : n-dim-complex
4. L : n-dim-complex
5. [%] : permutation(ℚCube(k);K;L)
6. c : {c:ℚCube(k)| (↑Inhabited(c)) ∧ (dim(c) = n ∈ ℤ)} 
7. (c ∈ L)
⊢ (c ∈ K)

3
1. k : ℕ
2. [n] : ℕ
3. K : n-dim-complex
4. L : n-dim-complex
5. [%] : ∀c:{c:ℚCube(k)| (↑Inhabited(c)) ∧ (dim(c) = n ∈ ℤ)} . ((c ∈ K) ⇐⇒ (c ∈ L))
⊢ permutation(ℚCube(k);K;L)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \mforall{}[n:\mBbbN{}]
        \mforall{}K,L:n-dim-complex.
            uiff(permutation(\mBbbQ{}Cube(k);K;L);\mforall{}c:\{c:\mBbbQ{}Cube(k)|  (\muparrow{}Inhabited(c))  \mwedge{}  (dim(c)  =  n)\} 
                                                                              ((c  \mmember{}  K)  \mLeftarrow{}{}\mRightarrow{}  (c  \mmember{}  L)))


By

---

Latex:
Auto

---

Home Index