# Zulip Chat Archive

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

ed 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