---

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
{ (Auto THEN ParallelOp -3 THEN Auto THEN (Decide i < n THENA 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
⊢ (∀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@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) ∈ ℚ)))

---

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

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

---

Home Index