Zulip Chat Archive

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.

Jujian Zhang (Sep 24 2020 at 14:41):

Please do PR those.

Reid Barton (Sep 24 2020 at 15:52):

#4241

Last updated: Dec 20 2023 at 11:08 UTC