---

Step * of Lemma member-le-max

∀[L:ℤ List]. ∀[x:ℤ].  x ≤ imax-list(L) supposing (x ∈ L)
BY
{ xxx(Auto THEN RWO "imax-list-ub" 0 THEN Auto)xxx }

1
1. L : ℤ List
2. x : ℤ
3. (x ∈ L)
⊢ (∃b∈L. x ≤ b)

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[x:\mBbbZ{}].    x  \mleq{}  imax-list(L)  supposing  (x  \mmember{}  L)


By

---

Latex:
xxx(Auto  THEN  RWO  "imax-list-ub"  0  THEN  Auto)xxx

---

Home Index