Zulip Chat Archive

Stream: general

Topic: intervals are infinite


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 24 2020 at 14:04):

We have stuff around docs#cardinal.mk_Icc_real

view this post on Zulip 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 ?

view this post on Zulip Johan Commelin (Sep 24 2020 at 14:08):

Aah, that's where I saw it!

view this post on Zulip 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...

view this post on Zulip Shing Tak Lam (Sep 24 2020 at 14:09):

@Jujian Zhang :up:

view this post on Zulip Jujian Zhang (Sep 24 2020 at 14:11):

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

view this post on Zulip Johan Commelin (Sep 24 2020 at 14:12):

Ooh, you don't need to close the PR

view this post on Zulip Johan Commelin (Sep 24 2020 at 14:13):

But I think some parts will need to be refactored abit

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jujian Zhang (Sep 24 2020 at 14:25):

Of course, I will do that!

view this post on Zulip Reid Barton (Sep 24 2020 at 14:38):

I can PR those I**.infinite lemmas.

view this post on Zulip Jujian Zhang (Sep 24 2020 at 14:41):

Please do PR those.

view this post on Zulip Reid Barton (Sep 24 2020 at 15:52):

#4241


Last updated: May 16 2021 at 05:21 UTC