Helper

crt_proj_pair_surj

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_2d

Type Lemma

Proof Lines 6

Signature

Lemma crt_proj_pair_surj (u2 u3 target : msg) (ppqq : ('F_p * 'F_p) * ('F_q * 'F_q)) : ppqq \in setX (fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target)) (fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq target)) -> exists vv, vv \in linear_fiber_2d u2 u3 target /\ crt_proj_pair vv = ppqq.

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