proposition: Lemma preimage_add T (R : numDomainType) (f g : T -> R) z : (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT) ((f @^-1` [set a]) `&` (g @^-1` [set z - a])).
proof: Proof. apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] []]. have : z - f x \in g @` setT. by rewrite inE /=; exists x=> //; rewrite -fgz addrC addKr. rewrite inE /= => -[x' _ gzf]; exists (z - g x')%R => /=. by exists x => //; rewrite gzf opprB addrC subrK. rewrite /preimage /=; split; first by rewrite gzf opprB addrC subrK. by rewrite gzf opprB addrC subrK -fgz addrC addKr. rewrite /preimage /= => [fxfy gzf]. by rewrite gzf -fxfy addrC subrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun