---

Step * 1 of Lemma member-le-max


1. L : ℤ List
2. x : ℤ
3. (x ∈ L)
⊢ (∃b∈L. x ≤ b)
BY
{ xxx(RepeatFor 2 (D -1) THEN With ⌜i⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  x  :  \mBbbZ{}
3.  (x  \mmember{}  L)
\mvdash{}  (\mexists{}b\mmember{}L.  x  \mleq{}  b)


By

---

Latex:
xxx(RepeatFor  2  (D  -1)  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index