Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 09:49 ed377e13

View on Github →

feat(analysis/convex): a local minimum of a convex function is a global minimum (#3613)

Estimated changes

Created src/analysis/convex/extrema.lean

added theorem is_min_on.of_is_local_min_of_convex_univ

added theorem is_min_on.of_is_local_min_on_of_convex_on

added theorem is_min_on.of_is_local_min_on_of_convex_on_Icc

Modified src/linear_algebra/affine_space.lean

added theorem affine_map.decomp'

added theorem affine_map.decomp

Created src/topology/algebra/affine.lean

added theorem affine_map.continuous_iff

added theorem affine_map.line_map_continuous