stuck

Stream: new members

[Shadman Sakib]

import data.real.basic

def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a
def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a

variable f : ℝ → ℝ

example : ¬ fn_has_ub (λ x, x) :=
begin
  intros fnub,
  cases fnub with a fnuba,
  unfold fn_ub at fnuba,

end

[Shadman Sakib]

I'm not sure how to affirm the x as a variable, since it is within a universal statement

[Yakov Pechersky]

specialize fnuba (a + 1)

[Kevin Buzzard]

The term fnuba is a term of type "for all..." so it is literally a function (which takes a number as input, and outputs a proof!). You could also do have h := fnuba (a+1).

[Shadman Sakib]

import data.real.basic

-- BEGIN
theorem not_monotone_iff {f : ℝ → ℝ}:
  ¬ monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y :=
by { rw monotone, push_neg }

example : ¬ monotone (λ x : ℝ, -x) :=
begin
  rw monotone,
  intros hab,

end
-- END

[Shadman Sakib]

How do I introduce a new hypothesis that says a <= b -> -b <= a

[Shadman Sakib]

Since a and b are not introduced

[Heather Macbeth]

Do you know a counterexample, that would disprove this? (That is, with actual numbers, like a = 7 and b = 17, or something.)

[Heather Macbeth]

Try finding the counterexample on paper and then applying hab to that counterexample.

[Patrick Massot]

Maybe Shadman is confused by the implicit binders

[Patrick Massot]

You can state something like

have key : (1 : ℝ) ≤ 2,
sorry,

and then specialize hab key (there is a faster way of course, but this should be clearer)

[Shadman Sakib]

Thank you! It worked.

[Shadman Sakib]

Another question when dealing with partial orders, I want to apply two hypotheses with exact to show the goal but I am not sure how.

[Shadman Sakib]

import tactic

-- BEGIN
variables {α : Type*} [partial_order α]
variables a b : α

example : a < b ↔ a ≤ b ∧ a ≠ b :=
begin
  rw lt_iff_le_not_le,
  split,
  { rintros ⟨h₀, h₁⟩,
    split,
    { exact h₀,},
    {
      sorry,
    }
  },
  {
    sorry,
  }
end
-- END

[Heather Macbeth]

There are two unproved pieces here -- which part are you asking for help on?

[Heather Macbeth]

You might like to read the instructions at the following link: #mwe which will help you ask more focused questions. For example, here you could have asked instead how to prove:

import tactic

-- BEGIN
variables {α : Type*} [partial_order α]
variables a b : α

example (h₀ : a ≤ b) (h₁ : ¬b ≤ a) :
  a ≠ b :=
begin
  sorry
end

(which is the goal state after all the work you show towards the first sorry).

[Shadman Sakib]

The first sorry

[Heather Macbeth]

OK! So, you need to prove that ¬b ≤ a implies a ≠ b. Do you know how to prove its contrapositive, that a = b implies b ≤ a?

[Shadman Sakib]

Ahh yes we would use rw after contraposing h\1.

[Shadman Sakib]

More than one way to do it, Thank you!