https://github.com/math-comp/analysis/blob/af08f5e9a149993baf055b8577020fef56f001ce/theories/topology_theory/topology_structure.v#L29 `finI_from` has moved to `filter.v`! shouldn't it be named `finI_from` be `open_finI_from`? (and `open_from`,`openU_from`?) `closed_bigsetU` -> `bigsetU_closed`
analysis/theories/topology_theory/topology_structure.v
Line 29 in af08f5e
finI_fromhas moved tofilter.v!shouldn't it be named
finI_frombeopen_finI_from?(and
open_from,openU_from?)closed_bigsetU->bigsetU_closed