Helper

pair_notin_fin_img_fst

File dumas2017dual/lib/extra_proba.v

Section proba_extra

Type Lemma

Proof Lines 17

Signature

Lemma pair_notin_fin_img_fst (T A B : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (a : A) (b : B) : a \notin fin_img X -> (a, b) \notin fin_img [% X, Y].

Description

If a is not in the image of X, then (a, b) cannot be in the joint image. This is used to show that pairs outside the support have zero probability.

Uses (0)

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

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats