Theoremsconvex, convex_ge, convex_gt, convex_le, convex_lt, convex_ge, convex_gt, convex_le, convex_lt, add, add_smul, add_smul_mem, add_smul_sub_mem, affine_image, affine_preimage, affinity, exists_mem_add_smul_eq, inter, is_linear_image, is_linear_preimage, lineMap_mem, linear_image, linear_preimage, mapsTo_lineMap, mem_smul_of_zero_mem, midpoint_mem, neg, openSegment_subset, ordConnected, prod, segment_subset, semilinear_image, setOf_const_imp, set_combo_subset, smul, smul_mem_of_zero_mem, smul_preimage, starConvex, starConvex_iff, sub, translate, translate_preimage_left, translate_preimage_right, vadd, Convex_subadditive_le, convex_iUnion, convex_sUnion, convex_ge, convex_gt, convex_le, convex_lt, convex_ge, convex_gt, convex_le, convex_lt, convex, convex_of_chain, convex, semilinear_range, convex, starConvex, coe_convexAddSubmonoid, convex_Icc, convex_Ici, convex_Ico, convex_Iic, convex_Iio, convex_Ioc, convex_Ioi, convex_Ioo, convex_empty, convex_halfSpace_ge, convex_halfSpace_gt, convex_halfSpace_le, convex_halfSpace_lt, convex_hyperplane, convex_iInter, convex_iInter₂, convex_iff_add_mem, convex_iff_div, convex_iff_forall_pos, convex_iff_openSegment_subset, convex_iff_ordConnected, convex_iff_pairwise_pos, convex_iff_pointwise_add_subset, convex_iff_segment_subset, convex_list_sum, convex_multiset_sum, convex_of_nonneg_surjective_algebraMap, convex_openSegment, convex_pi, convex_sInter, convex_segment, convex_singleton, convex_sum, convex_uIcc, convex_univ, convex_vadd, convex_zero, mem_convexAddSubmonoid | 100 |