---

Step * 1 of Lemma rv-le_witness


1. p : ℚ List
2. Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ
3. (∀q∈p.0 ≤ q)
4. n : ℕ
5. X : (ℕn ─→ ℕ||p||) ─→ ℚ
6. Y : (ℕn ─→ ℕ||p||) ─→ ℚ
7. ∀s:ℕn ─→ Outcome. ((X s) ≤ (Y s))@i
8. s : ℕn ─→ Outcome@i
⊢ Ax ∈ (X s) ≤ (Y s)
BY
{ (InstHyp [⌈s⌉] (-2)⋅ THEN Auto) }

1
1. p : ℚ List
2. Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ
3. (∀q∈p.0 ≤ q)
4. n : ℕ
5. X : (ℕn ─→ ℕ||p||) ─→ ℚ
6. Y : (ℕn ─→ ℕ||p||) ─→ ℚ
7. ∀s:ℕn ─→ Outcome. ((X s) ≤ (Y s))@i
8. s : ℕn ─→ Outcome@i
9. (X s) ≤ (Y s)
⊢ Ax ∈ (X s) ≤ (Y s)

---

Latex:



1.  p  :  \mBbbQ{}  List
2.  \mSigma{}0  \mleq{}  i  <  ||p||.  p[i]  =  1
3.  (\mforall{}q\mmember{}p.0  \mleq{}  q)
4.  n  :  \mBbbN{}
5.  X  :  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}||p||)  {}\mrightarrow{}  \mBbbQ{}
6.  Y  :  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}||p||)  {}\mrightarrow{}  \mBbbQ{}
7.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  \mleq{}  (Y  s))@i
8.  s  :  \mBbbN{}n  {}\mrightarrow{}  Outcome@i
\mvdash{}  Ax  \mmember{}  (X  s)  \mleq{}  (Y  s)


By

(InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index