---

Step * of Lemma imax-list_functionality

∀[L,L':ℤ List].  (imax-list(L) = imax-list(L') ∈ ℤ) supposing (set-equal(ℤ;L;L') and 0 < ||L||)
BY
{ (Auto THEN (InstLemma `imax-list-subset` [⌜L⌝;⌜L'⌝]⋅ THENA Auto)) }

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

2
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') ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[L,L':\mBbbZ{}  List].    (imax-list(L)  =  imax-list(L'))  supposing  (set-equal(\mBbbZ{};L;L')  and  0  <  ||L||)


By

---

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

---

Home Index