search

math-comp / analysis

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

`\oo` should be documented in `filter.v` #1342

Closed affeldt-aist closed 1 week ago

affeldt-aist commented 1 week ago

https://github.com/math-comp/analysis/blob/9033e920db0af923e48ea54cd8d5c69d2a94f590/theories/topology.v#L68

the notation has moved from toplogy.v to filter.v if I am not mistaken

affeldt-aist commented 1 week ago

eventually_filter, eventually_filterType, and eventually_pfilterType can maybe be moved from topology.v to filter.v