Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Elementary geometry (extension)
Spheres and lines in real Euclidean spaces
csph
Next ⟩
df-line
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
csph
Description:
Declare the syntax for spheres in generalized real Euclidean spaces.
Ref
Expression
Assertion
csph
class
Sphere