## Stream: maths

### Topic: help proving IVT

#### adriana (Apr 01 2020 at 02:55):

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 (Apr 01 2020 at 03:01):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:03):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:06):

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 (Apr 01 2020 at 03:06):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:09):

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 (Apr 01 2020 at 03:10):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:10):

Use cSup_le and le_cSup lemmas.

#### adriana (Apr 01 2020 at 03:28):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:35):

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

#### Yury G. Kudryashov (Apr 01 2020 at 03:37):

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 (Apr 01 2020 at 03:37):

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

#### adriana (Apr 01 2020 at 04:02):

thanks, I had the old version!

Last updated: May 11 2021 at 16:22 UTC