Commit 2023-03-28 12:18 910ab722

View on Github →

feat: port Analysis.Convex.Strict (#3148)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Strict.lean

added theorem Directed.strictConvex_unionᵢ

added theorem DirectedOn.strictConvex_unionₛ

added theorem IsOpen.strictConvex_iff

added theorem Set.Subsingleton.strictConvex

added theorem StrictConvex.add

added theorem StrictConvex.add_left

added theorem StrictConvex.add_right

added theorem StrictConvex.add_smul_mem

added theorem StrictConvex.add_smul_sub_mem

added theorem StrictConvex.affine_image

added theorem StrictConvex.affine_preimage

added theorem StrictConvex.affinity

added theorem StrictConvex.eq_of_openSegment_subset_frontier

added theorem StrictConvex.is_linear_image

added theorem StrictConvex.is_linear_preimage

added theorem StrictConvex.linear_image

added theorem StrictConvex.linear_preimage

added theorem StrictConvex.mem_smul_of_zero_mem

added theorem StrictConvex.neg

added theorem StrictConvex.openSegment_subset

added theorem StrictConvex.preimage_add_left

added theorem StrictConvex.preimage_add_right

added theorem StrictConvex.preimage_smul

added theorem StrictConvex.smul

added theorem StrictConvex.smul_mem_of_zero_mem

added theorem StrictConvex.sub

added theorem StrictConvex.vadd

added def StrictConvex

added theorem strictConvex_Icc

added theorem strictConvex_Ici

added theorem strictConvex_Ico

added theorem strictConvex_Iic

added theorem strictConvex_Iio

added theorem strictConvex_Ioc

added theorem strictConvex_Ioi

added theorem strictConvex_Ioo

added theorem strictConvex_empty

added theorem strictConvex_iff_convex

added theorem strictConvex_iff_div

added theorem strictConvex_iff_openSegment_subset

added theorem strictConvex_iff_ordConnected

added theorem strictConvex_singleton

added theorem strictConvex_uIcc

added theorem strictConvex_uIoc

added theorem strictConvex_univ