---

Step * 2 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
⊢ (∀s1,s2:ℕm ─→ Outcome.  ((∀j:ℕm. ((¬(j = i ∈ ℤ)) ⇒ ((s1 j) = (s2 j) ∈ Outcome))) ⇒ ((X s1) = (X s2) ∈ ℚ)))
∨ (∀s1,s2:ℕm ─→ Outcome.  ((∀j:ℕm. ((¬(j = i ∈ ℤ)) ⇒ ((s1 j) = (s2 j) ∈ Outcome))) ⇒ ((Y s1) = (Y s2) ∈ ℚ)))
BY
{ ((OrLeft  THEN Auto)
   THEN Try ((Fold `random-variable` 0 THEN Auto))
   THEN Try ((Fold `p-outcome` 0 THEN Auto))
   THEN Try ((DVar `p' THEN Complete (Auto)))) }

1
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) ∈ ℚ

---

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
\mvdash{}  (\mforall{}s1,s2:\mBbbN{}m  {}\mrightarrow{}  Outcome.    ((\mforall{}j:\mBbbN{}m.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((s1  j)  =  (s2  j))))  {}\mRightarrow{}  ((X  s1)  =  (X  s2))))
\mvee{}  (\mforall{}s1,s2:\mBbbN{}m  {}\mrightarrow{}  Outcome.    ((\mforall{}j:\mBbbN{}m.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((s1  j)  =  (s2  j))))  {}\mRightarrow{}  ((Y  s1)  =  (Y  s2))))


By

((OrLeft    THEN  Auto)
  THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
  THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
  THEN  Try  ((DVar  `p'  THEN  Complete  (Auto))))

---

Home Index