Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
Extended numbers and projective lines as sets
cinftyexpi

Next ⟩ df-bj-inftyexpi

Metamath Proof Explorer

Ascii
Structured

Syntax definition cinftyexpi

Description: Syntax for the function inftyexpi parameterizing CCinfty .

		Ref	Expression
	Assertion	cinftyexpi	class +∞eⁱ