Metamath Proof Explorer


Syntax definition cmopn

Description: Extend class notation with a function mapping each metric space to the family of its open sets.

Ref Expression
Assertion cmopn class MetOpen