IsOpen vs. IsClosed

Stream: new members

[Ilkka Törmä]

In Mathlib.Topology.Basic, the openness property IsOpen is implemented with def, while IsClosed is a class. What's the difference, why are they implemented this way, and why is neither of them a structure, which I thought would be the simplest way to wrap a property into a named object?

[Eric Wieser]

I'm very surprised to find out that docs#IsClosed is a class

[Eric Wieser]

The change was in !3#6552; where @Sébastien Gouëzel writes:

In lean-liquid, it would be useful that is_closed would be a class, to be able to infer a normed space structure on E/F when F is a closed subspace of a normed space E.

[Sébastien Gouëzel]

Yep, that's the reason: to infer nice behavior of quotient spaces G / H through typeclass inference, the typeclass inference mechanism needs to be able to see that H is closed, and this is only possible if IsClosed is a class.

[Johan Commelin]

fwiw, I think another option might have been to use [Fact (IsClosed H)].

[Kevin Buzzard]

We didn't have that option with things like [Fact (r < 1)] in LTE because making LT.lt a class would probably not have gone down well, but in this situation what are the advantages/disadvantages of the two choices (Fact / no Fact)? At the end of the day are they basically the same thing?

[Eric Wieser]

I think the main disadvantage is the weird asymmetry it creates between IsOpen and IsClosed

[Eric Wieser]

I think Fact would have a been a better choice here, as we use it already for things like ZMod.field

[Sébastien Gouëzel]

Maybe a good idea would be to also make IsOpena class, then, as quotienting by open subgroups also has very nice properties.

[Kevin Buzzard]

All open subgroups are closed though ;-) (consider a cover by cosets)

[Kyle Miller]

An idea I think would be very interesting is a new binder type that's like {...} binders, but which get solved for by assumption, especially if instances can use these binders.

It's like being able to use Fact with all local hypotheses without needing to create Fact instances.

[Mario Carneiro]

couldn't you just literally do (x : T := by assumption)?

[Mario Carneiro]

oh I missed the thing about instances

[Mario Carneiro]

I'm going to put another nickel in my jar of "reasons we should be allowed to have tactics in instance search"

[Kyle Miller]

Yeah, and it's also a bit different from default arguments because I'd want them to behave like implicit arguments (i.e., no passing them positionally)

[Mario Carneiro]

we could have {x : T := by assumption} too

[Kyle Miller]

An inspiration here is GHC's obscure implicit parameters feature, but it seems like it would see more use in Lean land, to help with passing facts around, rather than data.

[Kyle Miller]

Also, the feature I'm proposing is different in that the GHC one is by name, but mine is by type. Having some ability to try to capture variables by name would be interesting though -- we'd be able to recover parameter variables in some form.

[Sébastien Gouëzel]

Kevin Buzzard said:

All open subgroups are closed though ;-) (consider a cover by cosets)

Sure. But quotients by open subgroups are even better behaved than quotients by closed subgroups!