---

Step * 1 of Lemma imax-list-subset


1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. l_subset(ℤ;L;L')
5. 0 < ||L'||
⊢ (∀b∈L.b ≤ imax-list(L'))
BY
{ ((RWO "l_all_iff" 0 THEN Auto) THEN BLemma `imax-list-ub` THEN Auto)⋅ }

1
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. l_subset(ℤ;L;L')
5. 0 < ||L'||
6. b : ℤ@i
7. (b ∈ L)@i
⊢ (∃b1∈L'. b ≤ b1)

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  L'  :  \mBbbZ{}  List
3.  0  <  ||L||
4.  l\_subset(\mBbbZ{};L;L')
5.  0  <  ||L'||
\mvdash{}  (\mforall{}b\mmember{}L.b  \mleq{}  imax-list(L'))


By

---

Latex:
((RWO  "l\_all\_iff"  0  THEN  Auto)  THEN  BLemma  `imax-list-ub`  THEN  Auto)\mcdot{}

---

Home Index