---

Step * of Lemma index-min_wf

No Annotations
∀[zs:ℤ List+]. (index-min(zs) ∈ i:ℕ||zs|| × {x:ℤ| (x = zs[i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ zs) ⇒ (x ≤ z)))} )
BY
{ (Auto THEN D -1 THEN ListInd 1) }

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

2
1. u : ℤ
2. v : ℤ List
3. 0 < ||v|| ⇒ (index-min(v) ∈ i:ℕ||v|| × {x:ℤ| (x = v[i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ v) ⇒ (x ≤ z)))} )
⊢ 0 < ||[u / v]||
⇒ (index-min([u / v]) ∈ i:ℕ||[u / v]|| × {x:ℤ| (x = [u / v][i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ [u / v]) ⇒ (x ≤ z)))} )

---

Latex:

---

Latex:
No  Annotations
\mforall{}[zs:\mBbbZ{}  List\msupplus{}].  (index-min(zs)  \mmember{}  i:\mBbbN{}||zs||  \mtimes{}  \{x:\mBbbZ{}|  (x  =  zs[i])  \mwedge{}  (\mforall{}z:\mBbbZ{}.  ((z  \mmember{}  zs)  {}\mRightarrow{}  (x  \mleq{}  z)))\}  )


By

---

Latex:
(Auto  THEN  D  -1  THEN  ListInd  1)

---

Home Index