Helper

fdist_proj23_RV3

Section perm_extra

Type Lemma

Proof Lines 3

Lemma fdist_proj23_RV3 (TA TB TC : finType) (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}) : fdist_proj23 `p_[% X, Y, Z] = `p_[% Y, Z].

Projection of triple (X,Y,Z) onto (Y,Z) gives the joint distribution of (Y,Z). This connects fdist_proj23 with the random variable notation.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...