---

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

∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).  (rv-disjoint(p;n;X;Y) ⇒ (∀m:ℕ. rv-disjoint(p;m;X;Y) supposing n ≤ m))
BY
{ xxx(Auto THEN ParallelOp -3 THEN Auto THEN (Decide i < n THENA Auto))xxx }

1
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. Y : RandomVariable(p;n)
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) ∈ ℚ))))
6. m : ℕ
7. n ≤ m
8. i : ℕm
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) ∈ ℚ)))

2
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. Y : RandomVariable(p;n)
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) ∈ ℚ))))
6. m : ℕ
7. n ≤ m
8. i : ℕm
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) ∈ ℚ)))

---

Latex:

---

Latex:
\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y:RandomVariable(p;n).
    (rv-disjoint(p;n;X;Y)  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  rv-disjoint(p;m;X;Y)  supposing  n  \mleq{}  m))


By

---

Latex:
xxx(Auto  THEN  ParallelOp  -3  THEN  Auto  THEN  (Decide  i  <  n  THENA  Auto))xxx

---

Home Index