### Nuprl Lemma : rv-disjoint-rv-shift

`∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).`
`  (rv-disjoint(p;n;X;Y)`
`  `` (∀x,y:Outcome.  (rv-shift(x;X) = rv-shift(y;X) ∈ RandomVariable(p;n - 1)))`
`     ∨ (∀x,y:Outcome.  (rv-shift(x;Y) = rv-shift(y;Y) ∈ RandomVariable(p;n - 1))) `
`     supposing 0 < n)`

Proof

Definitions occuring in Statement :  rv-disjoint: `rv-disjoint(p;n;X;Y)` rv-shift: `rv-shift(x;X)` random-variable: `RandomVariable(p;n)` p-outcome: `Outcome` finite-prob-space: `FinProbSpace` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` subtract: `n - m` natural_number: `\$n` equal: `s = t ∈ T`
Lemmas :  member-less_than false_wf lelt_wf cons-seq_wf trivial-int-eq1 subtype_rel_self int_seg_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int subtract_wf decidable__le not-le-2 not-equal-2 sq_stable__le add_functionality_wrt_le add-associates add-zero zero-add le-add-cancel condition-implies-le add-commutes minus-add minus-zero minus-one-mul minus-minus add-swap decidable__lt less-iff-le le-add-cancel-alt not_wf equal-wf-T-base all_wf p-outcome_wf random-variable_wf le_wf rv-shift_wf less_than_wf rv-disjoint_wf nat_wf
\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y:RandomVariable(p;n).
(rv-disjoint(p;n;X;Y)
{}\mRightarrow{}  (\mforall{}x,y:Outcome.    (rv-shift(x;X)  =  rv-shift(y;X)))
\mvee{}  (\mforall{}x,y:Outcome.    (rv-shift(x;Y)  =  rv-shift(y;Y)))
supposing  0  <  n)

Date html generated: 2015_07_17-AM-07_59_06
Last ObjectModification: 2015_01_27-AM-11_23_15

Home Index