Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 04:03 ec5835d9

View on Github →

chore(order/*): use to_dual and of_dual in statements instead of implicit coercions between and α and order_dual α (#9593) Previously the meaning of the statement was hidden away in an invisible surprising typeclass argument. Before this change, the docs suggested the nonsensical statement that monotone f implies antitone f! image Most of the proof changes in this PR are a consequence of changing the interval lemmas, not the monotonicity or convexity ones.

Estimated changes

modified theorem concave_on.dual
modified theorem convex_on.dual
modified theorem strict_concave_on.dual
modified theorem strict_convex_on.dual
modified theorem set.dual_Icc
modified theorem set.dual_Ici
modified theorem set.dual_Ico
modified theorem set.dual_Iic
modified theorem set.dual_Iio
modified theorem set.dual_Ioc
modified theorem set.dual_Ioi
modified theorem set.dual_Ioo
modified theorem set.ord_connected.dual
modified theorem set.ord_connected_dual
modified theorem is_compl.to_order_dual
modified theorem is_extr_filter_dual_iff
modified theorem is_extr_on_dual_iff
modified theorem is_max_filter_dual_iff
modified theorem is_max_on_dual_iff
modified theorem is_min_filter_dual_iff
modified theorem is_min_on_dual_iff