Nuprl Definition : rv-disjoint
rv-disjoint(p;n;X;Y) ==
∀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) ∈ ℚ))))
Definitions occuring in Statement :
p-outcome: Outcome,
rationals: ℚ,
int_seg: {i..j-},
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
rv-disjoint
Latex:
rv-disjoint(p;n;X;Y) ==
\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)))))
Date html generated:
2016_05_15-PM-11_47_07
Last ObjectModification:
2008_02_27-PM-05_48_46
Theory : randomness
Home
Index