proposition: Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left T))))) p : (eps1 (P_delta_left T)) (x <|p|> y) = (eps1 (P_delta_left T)) x <|p|> (eps1 (P_delta_left T)) y.
proof: Proof. exact: scsl_hom_is_affine. Qed.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(boolp classical_sets) mathcomp(reals Rstruct) infotheo(classical_sets_ext Reals_ext ssrR fdist) infotheo(ssrR Reals_ext proba) infotheo(Reals_ext realType_ext) infotheo(fsdist convex necset) HB(structures) monae_lib hierarchy monad_lib proba_lib monad_model gcm_model category