This issue was opened at the end of a discussion (at least with @CohenCyril) where we felt the need for an inclusion of closed sets as a field of the topological mixin, instead of defining them from closures afterwards.
This was a long time ago, so I don't remember the arguments in favor of this.
NB(@affeldt-aist): this is a link to an important message in the conversation history #134 (comment) (so that it is not buried)
This issue was opened at the end of a discussion (at least with @CohenCyril) where we felt the need for an inclusion of closed sets as a field of the topological mixin, instead of defining them from closures afterwards.
This was a long time ago, so I don't remember the arguments in favor of this.
NB(@affeldt-aist): this is a link to an important message in the conversation history #134 (comment) (so that it is not buried)