Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 20:25 a52a54b6

View on Github →

chore(analysis/convex/basic): instance cleanup (#9466) Some lemmas were about f : whatever → 𝕜. They are now about f : whatever → β + a scalar instance between 𝕜 and β. Some add_comm_monoid assumptions are actually promotable to add_comm_group directly thanks to module.add_comm_monoid_to_add_comm_group. Related Zulip discussion.

Estimated changes

modified theorem convex.add
modified theorem convex.affine_image
modified theorem convex.affine_preimage
modified theorem convex.combo_affine_apply
modified theorem convex.combo_self
modified theorem convex.linear_image
modified def convex
modified theorem convex_Icc
modified theorem convex_Ici
modified theorem convex_Ico
modified theorem convex_Iic
modified theorem convex_Iio
modified theorem convex_Ioc
modified theorem convex_Ioi
modified theorem convex_Ioo
modified theorem convex_halfspace_ge
modified theorem convex_halfspace_gt
modified theorem convex_halfspace_le
modified theorem convex_halfspace_lt
modified theorem convex_hyperplane
modified theorem convex_interval
modified theorem convex_segment
modified theorem convex_std_simplex
modified theorem directed.convex_Union
modified theorem directed_on.convex_sUnion
modified theorem ite_eq_mem_std_simplex
modified def open_segment
modified def segment
modified theorem set.ord_connected.convex
modified def std_simplex
modified theorem mem_Icc_of_mem_std_simplex
modified theorem bounded_std_simplex
modified theorem compact_std_simplex
modified theorem is_closed_std_simplex