---

Step * 2 of Lemma q-max-exists


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

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

---

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{}qmax-list([u  /  v])\mkleeneclose{}  (D  0)\mcdot{}
  THEN  (Reduce  0  THEN  Auto')
  THEN  Try  ((BLemma  `qmax-list-member`  THEN  Auto)))\mcdot{}

---

Home Index