Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 13:24 62b8c1fa

View on Github →

feat(order/basic): Antitone functions (#9119) Define antitone and strict_anti. Use them where they already were used in expanded form. Rename lemmas accordingly. Provide a few more order_dual results, and rename monotone.order_dual to monotone.dual. Restructure order.basic. Now, monotone stuff can easily be singled out to go in a new file order.monotone if wanted. It represents 587 out of the 965 lines.

Estimated changes

added theorem antitone.map_max
added theorem antitone.map_min
modified theorem monotone.mul_strict_mono'
modified theorem strict_mono.mul'
modified theorem antitone_of_deriv_nonpos
deleted theorem convex_on_of_deriv_mono
added theorem strict_anti_on.comp
added theorem pell.strict_mono_x
added theorem pell.strict_mono_y
deleted theorem pell.x_increasing
deleted theorem pell.y_increasing
added theorem antitone.comp_monotone
added theorem antitone.reflect_lt
added def antitone
added theorem antitone_app
added theorem antitone_const
added theorem antitone_lam
added def antitone_on
added theorem antitone_on_univ
added theorem monotone.comp_antitone
modified theorem monotone.ne_of_lt_of_lt_int
modified theorem monotone.ne_of_lt_of_lt_nat
modified theorem monotone.reflect_lt
modified theorem monotone_app
modified theorem monotone_const
modified theorem monotone_id
modified theorem monotone_lam
added def monotone_on
added theorem monotone_on_univ
added theorem strict_anti.injective
added theorem strict_anti.le_iff_le
added theorem strict_anti.lt_iff_lt
added def strict_anti
modified theorem strict_anti_on.le_iff_le
modified theorem strict_anti_on.lt_iff_lt
modified def strict_anti_on
added theorem strict_anti_on_univ
deleted theorem strict_mono.comp
modified theorem strict_mono.id_le
modified theorem strict_mono.injective
modified theorem strict_mono.le_iff_le
modified theorem strict_mono.lt_iff_lt
deleted theorem strict_mono.monotone
deleted theorem strict_mono.order_dual
modified def strict_mono
modified theorem strict_mono_id
modified theorem strict_mono_nat_of_lt_succ
modified theorem strict_mono_on.le_iff_le
modified theorem strict_mono_on.lt_iff_lt
modified def strict_mono_on
added theorem strict_mono_on_univ
modified theorem tendsto_at_bot_csupr
modified theorem tendsto_at_bot_is_lub
modified theorem tendsto_at_bot_supr
modified theorem tendsto_at_top_cinfi
modified theorem tendsto_at_top_infi
modified theorem tendsto_at_top_is_glb