Question on monotonicity

Stream: new members

[Harry Pacitti]

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]

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]

or

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

[Chris B]

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]

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!