## Stream: general

### Topic: intervals are infinite

#### Johan Commelin (Sep 24 2020 at 13:58):

In #4235 the author proves that intervals are infinite. Isn't this already somewhere in mathlib? I couldn't find it.

#### Patrick Massot (Sep 24 2020 at 14:04):

We have stuff around docs#cardinal.mk_Icc_real

#### Reid Barton (Sep 24 2020 at 14:08):

Maybe you're thinking of https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/finite.lean#L49 ?

#### Johan Commelin (Sep 24 2020 at 14:08):

Aah, that's where I saw it!

#### Johan Commelin (Sep 24 2020 at 14:09):

What's the Zulip name of that PR author? They should know about both of these links...

#### Shing Tak Lam (Sep 24 2020 at 14:09):

@Jujian Zhang :up:

#### Jujian Zhang (Sep 24 2020 at 14:11):

That is me, I couldn’t find it. I will close the PR.

#### Johan Commelin (Sep 24 2020 at 14:12):

Ooh, you don't need to close the PR

#### Johan Commelin (Sep 24 2020 at 14:13):

But I think some parts will need to be refactored abit

#### Patrick Massot (Sep 24 2020 at 14:14):

See also the very first advice on https://leanprover-community.github.io/contribute/index.html. Preparing PRs is very time consuming so first asking whether something is already there can save a lot of efforts.

#### Patrick Massot (Sep 24 2020 at 14:14):

Don't worry, there are many things we don't have, so you won't run out of PR ideas.

#### Jujian Zhang (Sep 24 2020 at 14:17):

Let me reopen it with only the part stating if p evaluates to 0 on an interval then p is 0 (I need this for liouville theorem). This definitely is not part of mathlib right?

#### Johan Commelin (Sep 24 2020 at 14:22):

Yes, but like I commented, it's better to prove it for infinite sets, instead of intervals

#### Johan Commelin (Sep 24 2020 at 14:23):

And the when you use it, combine it with a lemma that says that Ioo/Ico/Ioc/Icc/... is infinite

#### Johan Commelin (Sep 24 2020 at 14:23):

Someone working with complex polynomials (or rational ones) or whatever, will be happy if you do htat.

#### Jujian Zhang (Sep 24 2020 at 14:25):

Of course, I will do that!

#### Reid Barton (Sep 24 2020 at 14:38):

I can PR those I**.infinite lemmas.