---

Step * 1 2 of Lemma int-problem-dimension_wf


1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ dim(inl <[u / v], %3>) ∈ ℕ
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  u  :  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\} 
3.  v  :  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
4.  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
\mvdash{}  dim(inl  <[u  /  v],  \%3>)  \mmember{}  \mBbbN{}


By

---

Latex:
ProveWfLemma

---

Home Index