---

Step * 2 1 of Lemma rv-disjoint-monotone-in-first


1. p : FinProbSpace@i
2. n : ℕ@i
3. X : RandomVariable(p;n)@i
4. Y : RandomVariable(p;n)@i
5. ∀i:ℕn
     ((∀s1,s2:ℕn ─→ Outcome.  ((∀j:ℕn. ((¬(j = i ∈ ℤ)) ⇒ ((s1 j) = (s2 j) ∈ Outcome))) ⇒ ((X s1) = (X s2) ∈ ℚ)))
     ∨ (∀s1,s2:ℕn ─→ Outcome.  ((∀j:ℕn. ((¬(j = i ∈ ℤ)) ⇒ ((s1 j) = (s2 j) ∈ Outcome))) ⇒ ((Y s1) = (Y s2) ∈ ℚ))))@i
6. m : ℕ@i
7. n ≤ m
8. i : ℕm@i
9. ¬i < n
10. s1 : ℕm ─→ Outcome@i
11. s2 : ℕm ─→ Outcome@i
12. ∀j:ℕm. ((¬(j = i ∈ ℤ)) ⇒ ((s1 j) = (s2 j) ∈ Outcome))@i
⊢ (X s1) = (X s2) ∈ ℚ
BY
{ (EqCD THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace@i
2.  n  :  \mBbbN{}@i
3.  X  :  RandomVariable(p;n)@i
4.  Y  :  RandomVariable(p;n)@i
5.  \mforall{}i:\mBbbN{}n
          ((\mforall{}s1,s2:\mBbbN{}n  {}\mrightarrow{}  Outcome.    ((\mforall{}j:\mBbbN{}n.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((s1  j)  =  (s2  j))))  {}\mRightarrow{}  ((X  s1)  =  (X  s2))))
          \mvee{}  (\mforall{}s1,s2:\mBbbN{}n  {}\mrightarrow{}  Outcome.    ((\mforall{}j:\mBbbN{}n.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((s1  j)  =  (s2  j))))  {}\mRightarrow{}  ((Y  s1)  =  (Y  s2)))))@i
6.  m  :  \mBbbN{}@i
7.  n  \mleq{}  m
8.  i  :  \mBbbN{}m@i
9.  \mneg{}i  <  n
10.  s1  :  \mBbbN{}m  {}\mrightarrow{}  Outcome@i
11.  s2  :  \mBbbN{}m  {}\mrightarrow{}  Outcome@i
12.  \mforall{}j:\mBbbN{}m.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((s1  j)  =  (s2  j)))@i
\mvdash{}  (X  s1)  =  (X  s2)


By

(EqCD  THEN  Auto)

---

Home Index