proposition: Lemma image_fsdistmap A B (x : gcm A) (k : choice_of_Type A -> gcm B) : fsdistmap k @` x = (gcm # k) x.
proof: Proof. rewrite /hierarchy.actm/= /actm 5!FCompE /category.actm/=. by rewrite /free_semiCompSemiLattConvType_mor/=; unlock. 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