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

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_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_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_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 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