antimono

Stream: maths

[Kevin Buzzard]

We don't seem to have

variables [preorder α] [preorder β]

def antimono (f : α → β) : Prop := ∀ ⦃a b⦄, a ≤ b → f b ≤ f a

Is this by design, i.e. if someone wants to use this idea then they are either supposed to spell it out (there are over 100 occurrences of antimono in mathlib) or use some monotone together with order_dual -- or is it just because nobody ever defined it and made a basic API for it? In order.basic we have a little API for monotone -- could one imagine a little API for antimono just after?

The reason I ask in that it comes up in #8853: Ines would like to use

import order.basic

theorem antitone_nat_of_succ_le {L : Type*} [preorder L] {f : ℕ → L}
  (hf : ∀ n : ℕ, f (n + 1) ≤ f n) :
  ∀ ⦃a b : ℕ⦄, a ≤ b → f b ≤ f a :=
@monotone_nat_of_le_succ (order_dual L) _ f hf

but I'm wondering whether the conclusion should just be antimono f (the corresponding conclusion for monotone_nat_of_le_succ is monotone f).

[Yaël Dillies]

Isn't contravariant to your antitone what covariant is to monotone?

[Kevin Buzzard]

Indeed, and the issue is that covariant is "the default thing" (e.g. our functors are covariant) and our definition of contravariant functors inserts an op in a random side of the equation rather than making a new definition.

[Yaël Dillies]

Yeah, supposedly you can make the above using monotone and that is arguably the right way to do it to avoid code duplication. But maybe defining antimono is worth it?

[François G. Dorais]

(Just to emphasize Yaël's subtle correction: antitone is an actual word and antimono is made-up.)

[Yaël Dillies]

What do people think of defining antitone? It'll probably lead to some code duplication but it would be nice to have for dot notation and stuff. It came up for me again because I need map_cInf_of_continuous_at_of_antitone (we currently only have map_cInf_of_continuous_at_of_monotone.

[Yaël Dillies]

We would then probably also define strict_anti, just as we have strict_mono.

[Sebastien Gouezel]

I'd prefer antimono over antitone, but otherwise I'm all for it.

[Kevin Buzzard]

Note François' comment above though

[Yaël Dillies]

#9119, for anyone interested

[Sebastien Gouezel]

ok for antitone, if that's a real word, but in this case it would be worth renaming the 106 occurences of antimono in mathlib to antitone :-)

[Frédéric Dupuis]

Maybe we could have a poll to choose between antitone and antimono?

[Yaël Dillies]

Sure

[Yaël Dillies]

/poll How should we name the dual notion of monotone?
antitone
antimono

[Reid Barton]

There was some (long) related discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/mathlib.20monotone.20definition/near/203536746

[Kalle Kytölä]

I used to be quite used to monotone meaning either increasing or decreasing. The terminology of increasing and decreasing (maybe with naming conventions incr and decr) would be intuitive and unambiguous (unless I overlook something), but it would be a massive change :frown:.

I'm not advocating for the massive change :smiley:. Both antitone and antimono seem anyway rather good (even the latter, despite not being a "real word", appears very logically cooked up given that mono is the established abbreviation for monotone).

[Kalle Kytölä]

Regarding the actual issue of introducing the property in the first place, I do remember occasionally struggling with using just monotone in combination with order_dual (and worrying about when that type synonym automatically gets all the structure needed). I think this antismth might help, but obviously don't have an informed opinion.

[Kevin Buzzard]

Wikipedia uses antitone in its article on monotonic functions

[Mario Carneiro]

The terminology of increasing and decreasing (maybe with naming conventions incr and decr) would be intuitive and unambiguous (unless I overlook something), but it would be a massive change :frown:.

Unfortunately, as mentioned in the previous thread, "increasing" is not unambiguous, because it may or may not mean "strictly increasing"

[Kalle Kytölä]

Indeed, the "strictness" remains equally ambiguous with both "increasing"/"decreasing" or "monotone"/"antixxxx". I only meant unambiguity of the directions (reversal or not of order relation), should have been clearer about that. Anyways, I think there are good options already and among them I couldn't decide how to vote.