Commit 2022-12-12 21:26 ac5a7cec

View on Github →

refactor(data/set/intervals/monotone): split (#17893) Also generalize&golf monotone_on.exists_monotone_extension and rename order.monotone to order.monotone.basic. Lean 4 version is leanprover-community/mathlib4#947

Estimated changes

Modified scripts/modules_used.lean

Modified src/algebra/covariant_and_contravariant.lean

Modified src/analysis/calculus/monotone.lean

Modified src/analysis/special_functions/trigonometric/deriv.lean

Modified src/data/int/basic.lean

Created src/data/set/intervals/iso_Ioo.lean

added def order_iso_Ioo_neg_one_one

Modified src/data/set/intervals/monotone.lean

deleted theorem antitone_on.exists_antitone_extension

deleted theorem monotone_of_odd_of_monotone_on_nonneg

deleted theorem monotone_on.exists_monotone_extension

deleted def order_iso_Ioo_neg_one_one

deleted theorem strict_mono_of_odd_strict_mono_on_nonneg

Modified src/order/iterate.lean

Modified src/order/lattice.lean

Renamed src/order/monotone.lean to src/order/monotone/basic.lean

Created src/order/monotone/extension.lean

added theorem antitone_on.exists_antitone_extension

added theorem monotone_on.exists_monotone_extension

Created src/order/monotone/odd.lean

added theorem antitone_of_odd_of_monotone_on_nonneg

added theorem monotone_of_odd_of_monotone_on_nonneg

added theorem strict_anti_of_odd_strict_anti_on_nonneg

added theorem strict_mono_of_odd_strict_mono_on_nonneg

Created src/order/monotone/union.lean

Modified src/topology/tietze_extension.lean