Zulip Chat Archive

Stream: new members

Topic: prop broadcasting


view this post on Zulip Lucas Viana (Jun 24 2020 at 01:41):

In topology it is common to have statements like "let a, b and c be open sets in M". In lean, I would write it as (a b c : set M) (is_open a) (is_open b) (is_open c). But this makes the statement very lengthy. Instead, it would be nice to have is_open to "broadcast" over a tuple of parameters, like is_open (a,b,c). Is there a way to make this possible?

view this post on Zulip Lucas Viana (Jun 24 2020 at 01:42):

(is_open as an example for the general idea)

view this post on Zulip Jalex Stark (Jun 24 2020 at 01:43):

you could make a subtype open_set M

view this post on Zulip Mario Carneiro (Jun 24 2020 at 01:43):

it's called opens in mathlib

view this post on Zulip Mario Carneiro (Jun 24 2020 at 01:44):

but the actual answer to your question is no, it's not possible

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 01:49):

You can do (a b c : opens M) though

view this post on Zulip Mario Carneiro (Jun 24 2020 at 01:51):

If you are okay with changing the statement to use opens instead of is_open it can be written this way, but if you actually want the statement to have is_open a,b,c you have to write it three times

view this post on Zulip Mario Carneiro (Jun 24 2020 at 01:52):

You can use variables to avoid repeating yourself though

view this post on Zulip Mario Carneiro (Jun 24 2020 at 01:53):

There are a lot of mathlib theorems with a bunch of typeclass arguments, and bundling them is not an option (or rather, it has its own downsides). Within the context of wanting a particular statement to come out at the end, variables is the only compression technique we have

view this post on Zulip Lucas Viana (Jun 24 2020 at 01:57):

Ok, thank you!


Last updated: May 14 2021 at 23:14 UTC