Notation inconsistency in `topology_structure.v`

[agontard]

The following three objects named open/op should have the same type:

analysis/theories/topology_theory/topology_structure.v

Line 94 in fe37644

open : set_system T;

analysis/theories/topology_theory/topology_structure.v

Line 452 in fe37644

Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) :=

analysis/theories/topology_theory/topology_structure.v

Line 456 in fe37644

op : set T -> Prop;

[affeldt-aist]

Thanks for reporting!
The change is implemented as PR #1805.