---

Step * 2 of Lemma q-min-exists


1. u : ℚ
2. v : ℚ List
⊢ ∃a:ℚ. ((a ∈ [u / v]) supposing ¬False ∧ (∀a'∈[u / v].a ≤ a'))
BY
{ (With ⌜qmin-list([u / v])⌝ (D 0)⋅ THEN (Reduce 0 THEN Auto') THEN Try ((BLemma `qmin-list-member` THEN Auto)))⋅ }

1
1. u : ℚ
2. v : ℚ List
3. (qmin-list([u / v]) ∈ [u / v])
⊢ (∀a'∈[u / v].qmin-list([u / v]) ≤ a')

---

Latex:

---

Latex:

1.  u  :  \mBbbQ{}
2.  v  :  \mBbbQ{}  List
\mvdash{}  \mexists{}a:\mBbbQ{}.  ((a  \mmember{}  [u  /  v])  supposing  \mneg{}False  \mwedge{}  (\mforall{}a'\mmember{}[u  /  v].a  \mleq{}  a'))


By

---

Latex:
(With  \mkleeneopen{}qmin-list([u  /  v])\mkleeneclose{}  (D  0)\mcdot{}
  THEN  (Reduce  0  THEN  Auto')
  THEN  Try  ((BLemma  `qmin-list-member`  THEN  Auto)))\mcdot{}

---

Home Index