help proving IVT

Stream: maths

[adriana]

hello, I am just getting started using lean and was wondering if anyone could help me out

I am trying to prove the IVT using the basic functions in lean. Right now, I have the following:

theorem intermediate_value {f : ℝ → ℝ} (Hf : continuous f)
{a b : ℝ} (Hab : a < b)
(Hav : f a < 0) (Hbv : f b > 0) :
∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
let K := {x | a<b ∧ x>a ∧ x<b ∧ f x <= 0},
let c := is_lub K,
--here I would like to use the definition of least upper bound, image of c, and continuity to say that f(c) is within epsilon of 0 but I'm not sure how to use the syntax of lean
end

[Yury G. Kudryashov]

is_lub is a predicate; you probably want let c := Sup K.

[Yury G. Kudryashov]

BTW, no need to include a < b in the definition of K. You already have it in Hab.

[Yury G. Kudryashov]

If you use non-strict inequalities everywhere, then you'll be able to say that K is closed, hence it contains its Sup (see cSup_mem_of_is_closed).

[Yury G. Kudryashov]

And you'll need to show that f x < 0 is impossible.

[Yury G. Kudryashov]

Or you can do something like (not tested)

rcases lt_trichotomy 0 (f c) with Hc | Hc | Hc,

In two cases you'll get to a contradiction, and in the middle case you'll need to show a < c and c < b.

[Yury G. Kudryashov]

It makes sense to prove a ≤ c and c ≤ b before doing rcases.

[Yury G. Kudryashov]

Use cSup_le and le_cSup lemmas.

[adriana]

which import statement do I need in order to use Sup?

[Yury G. Kudryashov]

What is your mathlib version? It older versions it is in lattice namespace (was changed a few weeks ago).

[Yury G. Kudryashov]

It is defined in order/complete_lattice; lemmas that work for reals are in order/conditionally_complete_lattice, and the latter file is imported by data/real/basic.

[Yury G. Kudryashov]

So, if you have real numbers, then you probably have Sup and most of its properties.

[adriana]

thanks, I had the old version!