Commit 2023-03-28 11:05 25d14ba8

View on Github →

feat: port Analysis.Convex.Basic (#3061)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Module.lean

Created Mathlib/Analysis/Convex/Basic.lean

added theorem AffineSubspace.convex

added theorem Antitone.convex_ge

added theorem Antitone.convex_gt

added theorem Antitone.convex_le

added theorem Antitone.convex_lt

added theorem AntitoneOn.convex_ge

added theorem AntitoneOn.convex_gt

added theorem AntitoneOn.convex_le

added theorem AntitoneOn.convex_lt

added theorem Convex.add

added theorem Convex.add_smul

added theorem Convex.add_smul_mem

added theorem Convex.add_smul_sub_mem

added theorem Convex.affine_image

added theorem Convex.affine_preimage

added theorem Convex.affinity

added theorem Convex.inter

added theorem Convex.is_linear_image

added theorem Convex.is_linear_preimage

added theorem Convex.linear_image

added theorem Convex.linear_preimage

added theorem Convex.mem_smul_of_zero_mem

added theorem Convex.neg

added theorem Convex.openSegment_subset

added theorem Convex.prod

added theorem Convex.segment_subset

added theorem Convex.smul

added theorem Convex.smul_mem_of_zero_mem

added theorem Convex.smul_preimage

added theorem Convex.starConvex

added theorem Convex.starConvex_iff

added theorem Convex.sub

added theorem Convex.translate

added theorem Convex.translate_preimage_left

added theorem Convex.translate_preimage_right

added theorem Convex.vadd

added def Convex

added theorem Directed.convex_unionᵢ

added theorem DirectedOn.convex_unionₛ

added theorem Monotone.convex_ge

added theorem Monotone.convex_gt

added theorem Monotone.convex_le

added theorem Monotone.convex_lt

added theorem MonotoneOn.convex_ge

added theorem MonotoneOn.convex_gt

added theorem MonotoneOn.convex_le

added theorem MonotoneOn.convex_lt

added theorem Set.OrdConnected.convex

added theorem Set.OrdConnected.convex_of_chain

added theorem convex_Icc

added theorem convex_Ici

added theorem convex_Ico

added theorem convex_Iic

added theorem convex_Iio

added theorem convex_Ioc

added theorem convex_Ioi

added theorem convex_Ioo

added theorem convex_empty

added theorem convex_halfspace_ge

added theorem convex_halfspace_gt

added theorem convex_halfspace_le

added theorem convex_halfspace_lt

added theorem convex_hyperplane

added theorem convex_iff_div

added theorem convex_iff_forall_pos

added theorem convex_iff_openSegment_subset

added theorem convex_iff_ordConnected

added theorem convex_iff_pairwise_pos

added theorem convex_iff_pointwise_add_subset

added theorem convex_iff_segment_subset

added theorem convex_interᵢ

added theorem convex_interᵢ₂

added theorem convex_interₛ

added theorem convex_openSegment

added theorem convex_pi

added theorem convex_segment

added theorem convex_singleton

added theorem convex_stdSimplex

added theorem convex_uIcc

added theorem convex_univ

added theorem ite_eq_mem_stdSimplex

added def stdSimplex

added theorem stdSimplex_eq_inter