mathlib3
48f557d5 - chore(analysis/convex/integral): use `variables` (#14592)

Commit
3 years ago
chore(analysis/convex/integral): use `variables` (#14592) * Move some implicit arguments to `variables`. * Move `ae_eq_const_or_exists_average_ne_compl` to the root namespace. * Add `ae_eq_const_or_norm_set_integral_lt_of_norm_le_const`.
Author
Parents
Loading