Metamath Proof Explorer


Syntax definition cnei

Description: Extend class notation with neighborhood relation for topologies.

Ref Expression
Assertion cnei class nei