---

Step * 1 of Lemma swap-intervals_wf


1. Gamma : CubicalSet{j}
⊢ csm-swap(Gamma;𝕀;𝕀) ∈ Gamma.𝕀.𝕀 j⟶ Gamma.𝕀.𝕀
BY
{ ((InstLemma `csm-swap_wf` [⌜parm{j}⌝;⌜parm{j}⌝;⌜Gamma⌝;⌜𝕀⌝;⌜𝕀⌝]⋅ THENA Auto)
   THEN RWO  "csm-interval-type" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
\mvdash{}  csm-swap(Gamma;\mBbbI{};\mBbbI{})  \mmember{}  Gamma.\mBbbI{}.\mBbbI{}  j{}\mrightarrow{}  Gamma.\mBbbI{}.\mBbbI{}


By

---

Latex:
((InstLemma  `csm-swap\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO    "csm-interval-type"  (-1)
  THEN  Auto)

---

Home Index