df-cp - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-cp		Structured version Visualization version GIF version

Definition df-cp 31557

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

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

**Detailed syntax breakdown of Definition df-cp**
Step	Hyp	Ref	Expression
1		ccp 31547	. 2 class Cp
2		ccpms 31523	. . 3 class cplMetSp
3		cqpa 31546	. . 3 class _Qp
4	2, 3	ccom 5118	. 2 class ( cplMetSp ∘ _Qp)
5	1, 4	wceq 1483	1 wff Cp = ( cplMetSp ∘ _Qp)

Colors of variables: wff setvar class

This definition is referenced by: (None)