closed of discrete

Stream: maths

[Johan Commelin]

Should

@[simp] lemma is_closed_discrete [topological_space α] [discrete_topology α] (s : set α) :
  is_closed s :=
is_open_compl_iff.1 $ (discrete_topology.eq_bot α).symm ▸ trivial

become an instance?

[Johan Commelin]

I don't really see a reason why not. Maybe it just wasn't touched during the is_closed-becomes-a-class refactor

[Floris van Doorn]

I missed the "make closed a class" refactor. But is_closed is now a class, but still (almost) all lemmas require it as explicit argument, and it has no instances (yet)? Interesting...

[Johan Commelin]

It's useful because a quotient of a normed group is again a normed group if the subgroup is closed.

[Johan Commelin]

I think this was the motivation for the refactor

[Sebastien Gouezel]

My feeling is that almost all statements with is_closed should be usual statements, not instances: the fact that it is a class is only useful for quotients of normed groups, as far as I can tell. Maybe statements that ensure that some subspaces are closed could also be registered as instances (for instance, it would make sense to register the fact that the kernel of a continuous linear map is closed).

[Johan Commelin]

@Sebastien Gouezel So you wouldn't make subspaces of discrete spaces closed by instance?

[Sebastien Gouezel]

I can't think of a situation where we would have a vector space with the discrete topology and we would use the fact that quotient spaces are normed. If you have an example of this situation in mind, we shoul definitely make this an instance. Otherwise, I'd just wait and add it if/when it is needed.

[Johan Commelin]

LTE

[Johan Commelin]

We need certain quotients of normed lattices to be normed lattices.

[Johan Commelin]

But I can certainly locally make an instance for those subgroups. We need it exactly once.

[Sebastien Gouezel]

Then let's make it an instance. I don't expect there will be that many instances ensuring that we have closed sets, so it shouldn't have any performance cost. Or rather, let's have both the lemma and the instance.