## 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