Commit 2023-03-24 17:26 e7167372

View on Github →

feat: port Analysis.Convex.Star (#3050)

<!-- The text above the `

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Star.lean

added theorem Set.OrdConnected.starConvex

added theorem StarConvex.add

added theorem StarConvex.add_left

added theorem StarConvex.add_right

added theorem StarConvex.add_smul_mem

added theorem StarConvex.add_smul_sub_mem

added theorem StarConvex.affine_image

added theorem StarConvex.affine_preimage

added theorem StarConvex.affinity

added theorem StarConvex.inter

added theorem StarConvex.is_linear_image

added theorem StarConvex.is_linear_preimage

added theorem StarConvex.linear_image

added theorem StarConvex.linear_preimage

added theorem StarConvex.mem

added theorem StarConvex.mem_smul

added theorem StarConvex.neg

added theorem StarConvex.openSegment_subset

added theorem StarConvex.preimage_add_left

added theorem StarConvex.preimage_add_right

added theorem StarConvex.preimage_smul

added theorem StarConvex.prod

added theorem StarConvex.segment_subset

added theorem StarConvex.smul

added theorem StarConvex.smul_mem

added theorem StarConvex.sub'

added theorem StarConvex.sub

added theorem StarConvex.union

added def StarConvex

added theorem starConvex_empty

added theorem starConvex_iff_div

added theorem starConvex_iff_forall_ne_pos

added theorem starConvex_iff_forall_pos

added theorem starConvex_iff_openSegment_subset

added theorem starConvex_iff_ordConnected

added theorem starConvex_iff_pointwise_add_subset

added theorem starConvex_iff_segment_subset

added theorem starConvex_interᵢ

added theorem starConvex_interₛ

added theorem starConvex_pi

added theorem starConvex_singleton

added theorem starConvex_unionᵢ

added theorem starConvex_unionₛ

added theorem starConvex_univ

added theorem starConvex_zero_iff