Theorem caufpm

Description: Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

	Ref	Expression
Assertion	caufpm	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge F\in \mathrm{Cau}\left(D\right)\right)\to F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscau	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(F\in \mathrm{Cau}\left(D\right)\leftrightarrow \left(F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge y}}\right):{\mathbb{Z}}_{\ge y}⟶F\left(y\right)\mathrm{ball}\left(D\right)x\right)\right)$$
2	1	simprbda	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge F\in \mathrm{Cau}\left(D\right)\right)\to F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)$$