Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-07 15:50 0e494afe

View on Github →

chore(order/*): Less order_dual abuse (#14008) Sanitize uses of order_dual by inserting the required of_dual and to_dual instead of type-ascripting. Also remove some uses which were not necessary. Those dated from the time where we did not have antitone functions.

Estimated changes

modified def decreasing_sequence
added theorem one_div_pow_anti
deleted theorem one_div_pow_mono
deleted theorem one_div_pow_strict_mono
modified theorem quasiconcave_on.dual
modified theorem quasiconvex_on.dual
modified theorem quasilinear_on.dual
added theorem finset.le_inf'_iff
deleted theorem order_dual.dual_compares
modified structure galois_coinsertion
modified def galois_insertion.dual