---

Step * 1 of Lemma index-min_wf


0 < ||[]|| ⇒ (index-min([]) ∈ i:ℕ||[]|| × {x:ℤ| (x = [][i] ∈ ℤ) ∧ (∀z@0:ℤ. ((z@0 ∈ []) ⇒ (x ≤ z@0)))} )
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

0  <  ||[]||  {}\mRightarrow{}  (index-min([])  \mmember{}  i:\mBbbN{}||[]||  \mtimes{}  \{x:\mBbbZ{}|  (x  =  [][i])  \mwedge{}  (\mforall{}z@0:\mBbbZ{}.  ((z@0  \mmember{}  [])  {}\mRightarrow{}  (x  \mleq{}  z@0)))\}  \000C)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index