Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-29 15:03 dc7de460

View on Github →

feat(analysis/convex): convex sets and functions (#834)

Estimated changes

Modified src/algebra/module.lean

added theorem is_linear_map.is_linear_map_neg

added theorem is_linear_map.is_linear_map_smul'

added theorem is_linear_map.is_linear_map_smul

Created src/analysis/convex.lean

added def convex

added theorem convex_Icc

added theorem convex_Ici

added theorem convex_Ico

added theorem convex_Iic

added theorem convex_Iio

added theorem convex_Inter

added theorem convex_Ioc

added theorem convex_Ioi

added theorem convex_Ioo

added theorem convex_add

added theorem convex_affinity

added theorem convex_ball

added theorem convex_closed_ball

added theorem convex_empty

added theorem convex_halfplane

added theorem convex_halfspace_ge

added theorem convex_halfspace_gt

added theorem convex_halfspace_im_gt

added theorem convex_halfspace_im_le

added theorem convex_halfspace_im_lge

added theorem convex_halfspace_im_lt

added theorem convex_halfspace_le

added theorem convex_halfspace_lt

added theorem convex_halfspace_re_gt

added theorem convex_halfspace_re_le

added theorem convex_halfspace_re_lge

added theorem convex_halfspace_re_lt

added theorem convex_iff:

added theorem convex_iff_div:

added theorem convex_inter

added theorem convex_le_of_convex_on

added theorem convex_linear_image'

added theorem convex_linear_image

added theorem convex_linear_preimage'

added theorem convex_linear_preimage

added theorem convex_lt_of_convex_on

added theorem convex_neg

added theorem convex_neg_preimage

added def convex_on

added theorem convex_on_add

added theorem convex_on_dist

added theorem convex_on_iff

added theorem convex_on_iff_div:

added theorem convex_on_linorder

added theorem convex_on_smul

added theorem convex_on_subset

added theorem convex_on_sum

added theorem convex_prod

added theorem convex_segment

added theorem convex_segment_iff

added theorem convex_singleton

added theorem convex_smul

added theorem convex_smul_preimage

added theorem convex_sub

added theorem convex_sum

added theorem convex_sum_iff

added theorem convex_translation

added theorem convex_univ

added theorem le_on_interval_of_convex_on

added theorem left_mem_segment

added theorem mem_segment_iff'

added theorem mem_segment_iff

added theorem right_mem_segment

added def segment

added theorem segment_eq_Icc

added theorem segment_symm

added theorem segment_translate

added theorem segment_translate_image

Modified src/data/set/intervals.lean

added theorem set.image_neg_Iic

added theorem set.image_neg_Iio

Modified src/linear_algebra/basic.lean

added theorem is_linear_map.is_linear_map_add

added theorem is_linear_map.is_linear_map_sub

Modified src/ring_theory/algebra.lean

added theorem complex.smul_im:

added theorem complex.smul_re: