prop broadcasting

Stream: new members

[Lucas Viana]

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?

[Lucas Viana]

(is_open as an example for the general idea)

[Jalex Stark]

you could make a subtype open_set M

[Mario Carneiro]

it's called opens in mathlib

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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

[Mario Carneiro]

You can use variables to avoid repeating yourself though

[Mario Carneiro]

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

[Lucas Viana]

Ok, thank you!