search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
200 stars 44 forks source link

Add closed sets to topological mixin #134

Open drouhling opened 5 years ago

drouhling commented 5 years ago

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.

affeldt-aist commented 1 year ago

It could maybe help to provide a description for this issue.

drouhling commented 1 year ago

It could maybe help to provide a description for this issue.

Edited.

CohenCyril commented 1 year ago

Thanks @drouhling.

The problematic is the following, and is easier to explain now we have HB: when using a factory of closed sets to build a topological space, if the structure of topological space only contains open sets, the function closed will not be definitionnally equal to the one given by the user in the factory, which is obviously undesirable since the user should not be able to tell the difference between a mixin and a factory.

Indeed it will be propositionally equal but it will most likely look like the double negation of the initial closed sets given by the user, after going through conversion to open set, through negation and closed sets again, with a second negation.