### Nuprl Lemma : rv-disjoint-shift

`∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n). ∀x:Outcome.`
`  rv-disjoint(p;n;X;Y) `` rv-disjoint(p;n - 1;rv-shift(x;X);rv-shift(x;Y)) 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` subtract: `n - m` natural_number: `\$n`
Lemmas :  member-less_than decidable__le false_wf not-le-2 sq_stable__le condition-implies-le minus-add minus-one-mul zero-add add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt less-iff-le subtract_wf lelt_wf cons-seq_wf minus-minus le_wf trivial-int-eq1 subtype_rel_self int_seg_wf not_wf equal_wf all_wf rationals_wf rv-shift_wf less_than_wf random-variable_wf rv-disjoint_wf p-outcome_wf nat_wf finite-prob-space_wf eq_int_wf bool_wf equal-wf-T-base assert_wf bnot_wf not-equal-2 minus-zero le-add-cancel-alt le-add-cancel2 or_wf iff_weakening_equal uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot
\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y:RandomVariable(p;n).  \mforall{}x:Outcome.
rv-disjoint(p;n;X;Y)  {}\mRightarrow{}  rv-disjoint(p;n  -  1;rv-shift(x;X);rv-shift(x;Y))  supposing  0  <  n

Date html generated: 2015_07_17-AM-07_59_23
Last ObjectModification: 2015_02_03-PM-09_45_38

Home Index