---

Step * 1 1 of Lemma imax-list-subset


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)
BY
{ (BLemma `l_exists_iff` THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  L'  :  \mBbbZ{}  List
3.  0  <  ||L||
4.  l\_subset(\mBbbZ{};L;L')
5.  0  <  ||L'||
6.  b  :  \mBbbZ{}@i
7.  (b  \mmember{}  L)@i
\mvdash{}  (\mexists{}b1\mmember{}L'.  b  \mleq{}  b1)


By

---

Latex:
(BLemma  `l\_exists\_iff`  THEN  Auto)

---

Home Index