Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Splitting fields
ccpms

Next ⟩ chlb

Metamath Proof Explorer

Ascii
Unicode

Syntax definition ccpms

Description: Completion of a metric space.

		Ref	Expression
	Assertion	ccpms	$class cplMetSp$