# Zulip Chat Archive

## Stream: new members

### Topic: Question on monotonicity

#### Harry Pacitti (Dec 24 2021 at 00:37):

I'm currently working through mathematics in lean and have been stuck on a problem for quite a while. Any help would be greatly appreciated. My current impression is that I should be able to use h monof and h' to show 1\<= 0, from which the goal would follow.

example :

¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=

begin

intro h,

let f := λ x : ℝ, (0 : ℝ),

have monof : monotone f,

{intros a b alab,

apply le_refl (f b),},

have h' : f 1 ≤ f 0,

from le_refl _,

end

#### Kevin Buzzard (Dec 24 2021 at 00:56):

Can you make a #mwe and use #backticks ? You can probably finish with

```
suffices : (1 : ℝ) ≤ 0, by linarith,
exact h monof h',
```

or some such thing (depending on what you're importing etc -- this is why a #mwe would help)

#### Kevin Buzzard (Dec 24 2021 at 00:56):

or

```
have h : (1 : ℝ) ≤ 0 := h monof h',
linarith,
```

#### Chris B (Dec 24 2021 at 00:59):

You can use `specialize`

to specialize hypotheses with other stuff.

```
example :
¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
intro h,
let f := λ x : ℝ, (0 : ℝ),
have monof : monotone f, {intros a b alab, apply le_refl (f b),},
have h' : f 1 ≤ f 0, from le_refl _,
specialize @h f monof 1 0 h',
linarith,
end
```

#### Harry Pacitti (Dec 24 2021 at 11:00):

Chris B said:

You can use

`specialize`

to specialize hypotheses with other stuff.`example : ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := begin intro h, let f := λ x : ℝ, (0 : ℝ), have monof : monotone f, {intros a b alab, apply le_refl (f b),}, have h' : f 1 ≤ f 0, from le_refl _, specialize @h f monof 1 0 h', linarith, end`

Thanks for the help!

Last updated: Dec 20 2023 at 11:08 UTC