Summary
- HOL-Analysis: fix latex generation
- Probability: fix proof
- Library: fix name Product_plus to Product_Plus
- HOL-Analysis: move Product_Vector and Inner_Product from Library
- HOL-Analysis: move Continuum_Not_Denumerable from Library
- HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
- HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)