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,
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,
rationals: ℚ
Definitions :
or: P ∨ Q,
function: x:A ─→ B[x],
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
implies: P ⇒ Q,
not: ¬A,
int: ℤ,
p-outcome: Outcome,
equal: s = t ∈ T,
rationals: ℚ,
apply: f a
FDL editor aliases :
rv-disjoint
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:
2015_07_17-AM-07_59_04
Last ObjectModification:
2008_02_27-PM-05_48_46
Home
Index