Nuprl 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))


Proof




Definitions occuring in Statement :  rv-disjoint: rv-disjoint(p;n;X;Y) random-variable: RandomVariable(p;n) finite-prob-space: FinProbSpace nat: uimplies: supposing a le: A ≤ B all: x:A. B[x] implies:  Q
Lemmas :  less_than_wf decidable__lt int_seg_wf le_wf nat_wf rv-disjoint_wf random-variable_wf finite-prob-space_wf equal-wf-T-base all_wf equal_wf not_wf iff_weakening_equal less_than_transitivity1 int-subtype-rationals subtype_rel_self false_wf subtype_rel-int_seg l_member_wf Error :qle_wf,  l_all_wf2 sq_stable__le select_wf length_wf Error :qsum_wf,  rationals_wf p-outcome_wf subtype_rel_dep_function lelt_wf or_wf le-add-cancel2 add_functionality_wrt_le less-iff-le zero-add add-commutes add-swap minus-one-mul minus-add add-associates condition-implies-le not-le-2 decidable__le not-equal-2
\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))



Date html generated: 2015_07_17-AM-07_59_16
Last ObjectModification: 2015_07_16-AM-09_52_15

Home Index