---

Step * 2 of Lemma imax-list_functionality


1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
⊢ imax-list(L) = imax-list(L') ∈ ℤ
BY
{ (InstLemma `imax-list-subset` [⌜L'⌝;⌜L⌝]⋅ THENA Auto)⋅ }

1
.....antecedent..... 
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
⊢ 0 < ||L'||

2
.....antecedent..... 
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
⊢ l_subset(ℤ;L';L)

3
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
6. imax-list(L') ≤ imax-list(L)
⊢ imax-list(L) = imax-list(L') ∈ ℤ

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  L'  :  \mBbbZ{}  List
3.  0  <  ||L||
4.  set-equal(\mBbbZ{};L;L')
5.  imax-list(L)  \mleq{}  imax-list(L')
\mvdash{}  imax-list(L)  =  imax-list(L')


By

---

Latex:
(InstLemma  `imax-list-subset`  [\mkleeneopen{}L'\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index