Definition df-cp

Description: Define the metric completion of the algebraic completion of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-cp	⊢ Cp = ( cplMetSp ∘ _Qp )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccp	⊢ Cp
1		ccpms	⊢ cplMetSp
2		cqpa	⊢ _Qp
3	1 2	ccom	⊢ ( cplMetSp ∘ _Qp )
4	0 3	wceq	⊢ Cp = ( cplMetSp ∘ _Qp )