# Zulip Chat Archive

## Stream: new members

### Topic: monotone decreasing ```ℕ → ℕ```

#### Damiano Testa (Sep 09 2020 at 08:25):

Dear All,

I want to prove the lemma below, ~~stating essentially~~ which is an easy consequence of the fact that the map `rev_at`

is monotone decreasing. If I formulated it correctly, it says the following. Given a finite subset `s`

of `ℕ`

, the "reflected" set, formed of the elements `(max s) - e`

as `e ∈ s`

, has as maximum the "reflection" of the minimum `(max s) - (min s)`

.

I found `monotone`

, but I think that it is only non-decreasing. Note that, due to how subtraction works, every natural number above `max s`

squashes to `0`

: this is not a problem, since I never evaluate at those naturals.

Thanks!

```
import tactic
open finset
def rev_at (N : ℕ) : ℕ → ℕ := λ i : ℕ , (N-i)
lemma min_max {s : finset ℕ} {hs : s.nonempty} : max' (image (rev_at (max' s hs)) s) (by exact nonempty.image hs (rev_at (max' s hs))) = rev_at (max' s hs) (min' s hs) :=
begin
sorry,
end
```

#### Kenny Lau (Sep 09 2020 at 08:29):

I think there's a simpler way to state that a map is monotone decreasing

#### Damiano Testa (Sep 09 2020 at 08:30):

I'd be happy to know how to do it! I tried looking for it, but could not find it...

#### Kenny Lau (Sep 09 2020 at 08:30):

`x <= y -> f y <= f x`

?

#### Damiano Testa (Sep 09 2020 at 08:30):

(I found a lot of lemmas with maxs, mins, sups,... for monotone non-decreasing maps, but I could not find monotone non-increasing lemmas

#### Damiano Testa (Sep 09 2020 at 08:31):

Kenny Lau said:

`x <= y -> f y <= f x`

?

The map `rev_at`

satisfies this condition. Is there then a lemma saying what I want?

#### Kenny Lau (Sep 09 2020 at 08:32):

I'm just objecting your statement that `min_max`

is the right way to say that a map is monotone decreasing

#### Damiano Testa (Sep 09 2020 at 08:33):

Kenny Lau said:

I'm just objecting your statement that

`min_max`

is the right way to say that a map is monotone decreasing

Ah, I see! I had meant that my lemma is an immediate consequence of the fact that `rev_at`

is monotone non-increasing! Sorry! I will correct it.

#### Kenny Lau (Sep 09 2020 at 08:33):

then generalize the lemma and remove `rev_at`

#### Damiano Testa (Sep 09 2020 at 08:35):

Ok, how do I introduce the hypothesis that a map N->N is monotone non-increasing? The lemma that I stated already exists for monotone non-increasing maps and I would like to use something that is already available, if possible

#### Kenny Lau (Sep 09 2020 at 08:36):

just say that `x <= y -> f y <= f x`

#### Kenny Lau (Sep 09 2020 at 08:36):

also generalize the domain and codomain

#### Damiano Testa (Sep 09 2020 at 08:48):

Is this what you had in mind? The lemma that I want follows easily from the statement below.

```
import tactic
open finset
def mon {α β : Type} [decidable_linear_order α] [decidable_linear_order β] (f : α → β) := ∀ (x y : α), x ≤ y → f y ≤ f x
lemma min_max {α β : Type} [decidable_linear_order α] [decidable_linear_order β] {s : finset α} {hs : s.nonempty} {f : α → β} {mf : mon f} : max' (image f s) (by exact nonempty.image hs f) = f (min' s hs) :=
begin
sorry,
end
```

#### Damiano Testa (Sep 09 2020 at 08:49):

But I still cannot find this last statement in mathlib...

#### Kenny Lau (Sep 09 2020 at 08:57):

yeah now you can prove it

#### Kenny Lau (Sep 09 2020 at 08:57):

you don't need decidable for `mon`

#### Kenny Lau (Sep 09 2020 at 08:57):

also make it `\{{x y : \a\}}`

#### Damiano Testa (Sep 09 2020 at 08:58):

Kenny Lau said:

also make it

`\{{x y : \a\}}`

What does this mean?

#### Johan Commelin (Sep 09 2020 at 08:59):

It's something in between `{x y}`

and `(x y)`

#### Johan Commelin (Sep 09 2020 at 09:00):

The thing is... if you use `(x y)`

, then you have to write them down all the time, when you use your lemma

#### Johan Commelin (Sep 09 2020 at 09:01):

With `{x y}`

and `{{x y}}`

you tell Lean that you want it to figure them out itself.

#### Johan Commelin (Sep 09 2020 at 09:01):

But the difference between the two is how greedy Lean is when trying to do this.

#### Damiano Testa (Sep 09 2020 at 09:01):

ok, i knew one curly bracket, but not two

#### Damiano Testa (Sep 09 2020 at 09:01):

i see, thanks!

#### Johan Commelin (Sep 09 2020 at 09:01):

With `{x y}`

it will try to figure out `x`

and `y`

as soon as possible.

#### Johan Commelin (Sep 09 2020 at 09:02):

But with `{{x y}}`

it will leave them as part of the expression, until you start filling in arguments that come after them.

#### Damiano Testa (Sep 09 2020 at 09:02):

so, I should try to prove this lemma, then?

```
def mon {α β : Type*} [linear_order α] [linear_order β] (f : α → β) := ∀ ⦃x y : α⦄, x ≤ y → f y ≤ f x
lemma min_max_mon {α β : Type*} [decidable_linear_order α] [decidable_linear_order β]
{s : finset α} (hs : s.nonempty) {f : α → β} (mf : mon f) :
max' (image f s) (by exact nonempty.image hs f) = f (min' s hs) :=
begin
sorry,
end
```

#### Kenny Lau (Sep 09 2020 at 09:03):

make `hs`

explicit

#### Kenny Lau (Sep 09 2020 at 09:03):

and also `mf`

#### Kenny Lau (Sep 09 2020 at 09:04):

and also use more newlines

#### Kenny Lau (Sep 09 2020 at 09:05):

wow we can copy codes now?

#### Kenny Lau (Sep 09 2020 at 09:05):

also indentation is 2 spaces not 1

#### Kenny Lau (Sep 09 2020 at 09:05):

also `\{{x`

not `\{{ x`

#### Damiano Testa (Sep 09 2020 at 09:05):

(I have been updating the code above, so your statements do not seem to make sense!)

#### Kenny Lau (Sep 09 2020 at 09:07):

also `hs.image f`

#### Damiano Testa (Sep 09 2020 at 09:09):

I cannot believe how many issues there were with my coding grammar...

#### Kenny Lau (Sep 09 2020 at 09:10):

`by exact`

can go

#### Damiano Testa (Sep 09 2020 at 09:10):

One question: using `{α β : Type*}`

can the universes of `α`

and `β`

be different?

A: Yes.

#### Kenny Lau (Sep 09 2020 at 09:11):

what does the goal say?

#### Damiano Testa (Sep 09 2020 at 09:11):

```
1 goal
α: Type u_1
β: Type u_2
_inst_1: decidable_linear_order α
_inst_2: decidable_linear_order β
s: finset α
hs: s.nonempty
f: α → β
mf: mon f
⊢ (image f s).max' _ = f (s.min' hs)
```

#### Damiano Testa (Sep 09 2020 at 09:12):

good, thanks!

#### Damiano Testa (Sep 09 2020 at 12:31):

In case anyone is keeping track, below is a solution to my question!

Thanks for @Kenny Lau and @Johan Commelin for helping me!

```
import tactic
open finset
def mon {α β : Type*} [linear_order α] [linear_order β] (f : α → β) := ∀ ⦃x y : α⦄, x ≤ y → f y ≤ f x
lemma min_max_mon {α β : Type*} [decidable_linear_order α] [decidable_linear_order β]
{s : finset α} (hs : s.nonempty) {f : α → β} (mf : mon f) :
max' (image f s) (hs.image f) = f (min' s hs) :=
begin
apply le_antisymm,
{ refine (image f s).max'_le (nonempty.image hs f) (f (min' s hs)) _,
intros x hx,
rw mem_image at hx,
rcases hx with ⟨ b , bs , rfl⟩,
apply mf,
apply min'_le,
assumption, },
{ apply le_max',
refine mem_image_of_mem f _,
exact min'_mem s hs, },
end
def rev_at (N : ℕ) : ℕ → ℕ := λ i : ℕ , (N-i)
lemma min_max {s : finset ℕ} {hs : s.nonempty} : max' (image (rev_at (max' s hs)) s) (by exact nonempty.image hs (rev_at (max' s hs))) = rev_at (max' s hs) (min' s hs) :=
begin
refine min_max_mon hs _,
intros x y hxy,
unfold rev_at,
omega,
end
```

#### Kenny Lau (Sep 09 2020 at 12:39):

we should really have `finset.forall_mem_image`

#### Kenny Lau (Sep 09 2020 at 12:39):

like `list.forall_mem_map`

iirc

Last updated: May 08 2021 at 09:11 UTC