cmopn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cmopn		Structured version Visualization version GIF version

Syntax Definition cmopn 20596

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

**Assertion**
Ref	Expression
cmopn	class MetOpen

See definition df-mopn 20602 for more information.

Colors of variables: wff setvar class