The name of open_nbhs is misleading as it does not contain the nbhs property, and makes searching difficult. Can it be renamed mem_open (or else) and can open_nbhs_nbhs be renamed as mem_open_nbhs ?
Definition open_nbhs (p : T) (A : set T) := open A /\ A p.
Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A.
has a circular flavor : one can think that open_nbhs is the conjunction of open and nbhs and that the lemma looks circular.
The documentation in topology_structure is itself is also a bit misleading, as it interprets the definition instead of describing it.
The name of
open_nbhsis misleading as it does not contain thenbhsproperty, and makes searching difficult. Can it be renamedmem_open(or else) and canopen_nbhs_nbhsbe renamed asmem_open_nbhs?Definition open_nbhs (p : T) (A : set T) := open A /\ A p.Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A.has a circular flavor : one can think that
open_nbhsis the conjunction ofopenandnbhsand that the lemma looks circular.The documentation in
topology_structureis itself is also a bit misleading, as it interprets the definition instead of describing it.