Theorem convex_iff_add_mem

Modification history

2025-05-07 04:11
Mathlib/Analysis/Convex/Basic.lean
feat(MeasureTheory): integral is monotone/convex if the integrand is monotone/convex (#24341) …
Added convex_iff_add_memView on Github →