---

Step * of Lemma q-min-exists

∀as:ℚ List. ∃a:ℚ. ((a ∈ as) supposing ¬↑null(as) ∧ (∀a'∈as.a ≤ a'))
BY
{ xxx(xxxAutoxxx THEN D 1 THEN Reduce 0)xxx }

1
∃a:ℚ. ((a ∈ []) supposing ¬True ∧ (∀a'∈[].a ≤ a'))

2
1. u : ℚ
2. v : ℚ List
⊢ ∃a:ℚ. ((a ∈ [u / v]) supposing ¬False ∧ (∀a'∈[u / v].a ≤ a'))

---

Latex:

---

Latex:
\mforall{}as:\mBbbQ{}  List.  \mexists{}a:\mBbbQ{}.  ((a  \mmember{}  as)  supposing  \mneg{}\muparrow{}null(as)  \mwedge{}  (\mforall{}a'\mmember{}as.a  \mleq{}  a'))


By

---

Latex:
xxx(xxxAutoxxx  THEN  D  1  THEN  Reduce  0)xxx

---

Home Index