Syntax Definition csqr 4727

Description: Extend class notation to include positive square root of a positive real number.

Assertion

Ref	Expression
csqr	class sqr

See definition df-sqr 4728 for more information.

metamath.org