---

Step * of Lemma csm-canonical-section-face-type-0

∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[phi:𝔽(I)].
  ((canonical-section(();𝔽;I+i;⋅;s(phi)))<(i0)> = canonical-section(();𝔽;I;⋅;phi) ∈ {formal-cube(I) ⊢ _:𝔽})
BY
{ ((RWO  "csm-canonical-section-face-type<" 0 THEN Auto) THEN EqCDA) }

1
.....subterm..... T:t
5:n
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
⊢ (i0)(s(phi)) = phi ∈ 𝔽(⋅)

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[phi:\mBbbF{}(I)].
    ((canonical-section(();\mBbbF{};I+i;\mcdot{};s(phi)))<(i0)>  =  canonical-section(();\mBbbF{};I;\mcdot{};phi))


By

---

Latex:
((RWO    "csm-canonical-section-face-type<"  0  THEN  Auto)  THEN  EqCDA)

---

Home Index