---

Step * of Lemma simplex-face-face

∀[n:ℤ]. ∀[v:Δ(n)]. ∀[i,j:ℕn + 2].
  simplex-face(simplex-face(v;i);j) = simplex-face(simplex-face(v;j);i + 1) ∈ Δ(n + 2) supposing j ≤ i
BY
{ Auto }

1
1. n : ℤ
2. v : Δ(n)
3. i : ℕn + 2
4. j : ℕn + 2
5. j ≤ i
⊢ simplex-face(simplex-face(v;i);j) = simplex-face(simplex-face(v;j);i + 1) ∈ Δ(n + 2)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[v:\mDelta{}(n)].  \mforall{}[i,j:\mBbbN{}n  +  2].
    simplex-face(simplex-face(v;i);j)  =  simplex-face(simplex-face(v;j);i  +  1)  supposing  j  \mleq{}  i


By

---

Latex:
Auto

---

Home Index