## Stream: Is there code for X?

### Topic: monotone increasing or decreasing subsequence

#### Kevin Buzzard (Feb 16 2021 at 00:17):

Do we have either this definition or some form of this theorem? It came up in #6208.

import order.basic

def antitone {α β : Type*} [preorder α] [preorder β]
(f : α → β) := ∀⦃a b⦄, a ≤ b → f b ≤ f a

example (α : Type) [linear_order α] (f : ℕ → α) : ∃ φ : ℕ → ℕ,
strict_mono φ ∧ (monotone (f ∘ φ) ∨ antitone (f ∘ φ)) := sorry


The proof I know is sketched in my review of the PR: you do a case split on whether the set {n | \forall m > n, f m < f n} is finite or infinite. The Bolzano-Weierstrass theorem for R follows without too much trouble from this (because a monotonic bounded sequence converges) and this was the proof I learnt as an undergrad, however we seem to have some fancier proof of BW in mathlib.

The reason it's relevant is that if furthermore f is injective then one can guarantee that f ∘ φ is strict mono or antimono, and deduce that if alpha is an infinite linearly ordered type then at least one of alpha and its order-dual must be not well-founded -- the naturals inject into any infinite type.

#### Eric Wieser (Feb 16 2021 at 00:18):

I imagine antitone follows from some application of order_dual

#### Kevin Buzzard (Feb 16 2021 at 00:19):

Sure, but I still need a name for it because if I only have f ∘ φ then it's hard to get my hands on the order_dual unless you want the usual @ _-fest.

#### Eric Wieser (Feb 16 2021 at 00:19):

import order.basic

def antitone {α β : Type*} [preorder α] [preorder β]
(f : α → β) := ∀⦃a b⦄, a ≤ b → f b ≤ f a

def antitone' {α β : Type*} [preorder α] [preorder β]
(f : α → β) := @monotone α (order_dual β) _ _ f

example {α β : Type*} [preorder α] [preorder β] (f : α → β):
antitone' f = antitone f := rfl


#### Eric Wieser (Feb 16 2021 at 00:19):

So I don't know if we have a name, but you can pick up all the existing lemmas by using that antitone' definition

#### Kevin Buzzard (Feb 16 2021 at 00:20):

Sure, but if you don't define it then you'll just get the @ _-fest in the statement of the theorem.

#### Eric Wieser (Feb 16 2021 at 00:20):

I agree - I'm just saying we have a full implementation, it just doesn't have a usable name yet :)

#### Kevin Buzzard (Feb 16 2021 at 00:22):

Anyway, I would be happy to have the example phrased in whatever way, the real question is whether it's there already.

#### Aaron Anderson (Feb 16 2021 at 02:52):

I added a version of this theorem in #6208, and used it again in #6226.

#### Aaron Anderson (Feb 16 2021 at 02:54):

If it turns out it does already exist, I'd be happy to use the existing form, but I don't think it does, and it saved me a lot of code in those two PRs.

#### Aaron Anderson (Feb 16 2021 at 02:59):

My formulation refers to a general relation, and so doesn't need antitone to be defined, but there are some good corollaries that could be defined using monotone, etc.

Last updated: May 16 2021 at 05:21 UTC