Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 ec48e3b9

View on Github →

feat(analysis/convex/strict): Strictly convex sets (#10648) This defines strictly convex sets.

Estimated changes

Created src/analysis/convex/strict.lean

added theorem directed.strict_convex_Union

added theorem directed_on.strict_convex_sUnion

added theorem is_open.strict_convex_iff

added theorem set.subsingleton.strict_convex

added theorem strict_convex.add

added theorem strict_convex.add_left

added theorem strict_convex.add_right

added theorem strict_convex.add_smul_mem

added theorem strict_convex.add_smul_sub_mem

added theorem strict_convex.affine_image

added theorem strict_convex.affine_preimage

added theorem strict_convex.affinity

added theorem strict_convex.eq_of_open_segment_subset_frontier

added theorem strict_convex.is_linear_image

added theorem strict_convex.is_linear_preimage

added theorem strict_convex.linear_image

added theorem strict_convex.linear_preimage

added theorem strict_convex.mem_smul_of_zero_mem

added theorem strict_convex.neg

added theorem strict_convex.neg_preimage

added theorem strict_convex.open_segment_subset

added theorem strict_convex.preimage_add_left

added theorem strict_convex.preimage_add_right

added theorem strict_convex.preimage_smul

added theorem strict_convex.smul

added theorem strict_convex.smul_mem_of_zero_mem

added def strict_convex

added theorem strict_convex_Icc

added theorem strict_convex_Ici

added theorem strict_convex_Ico

added theorem strict_convex_Iic

added theorem strict_convex_Iio

added theorem strict_convex_Ioc

added theorem strict_convex_Ioi

added theorem strict_convex_Ioo

added theorem strict_convex_empty

added theorem strict_convex_iff_convex

added theorem strict_convex_iff_div

added theorem strict_convex_iff_open_segment_subset

added theorem strict_convex_iff_ord_connected

added theorem strict_convex_interval

added theorem strict_convex_singleton

added theorem strict_convex_univ