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 30811

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 30801	. 2 class Cp
2		ccpms 30777	. . 3 class cplMetSp
3		cqpa 30800	. . 3 class _Qp
4	2, 3	ccom 5042	. 2 class ( cplMetSp ∘ _Qp)
5	1, 4	wceq 1475	1 wff Cp = ( cplMetSp ∘ _Qp)

Colors of variables: wff setvar class

This definition is referenced by: (None)