Mathlib Changelog
v3
Changelog
About
Github
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: