ulmcau2

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k , m the functions F ( k ) and F ( m ) are uniformly within x of each other on S . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	ulmcau.z	$⊢ Z = ℤ_{\geq M}$
	ulmcau.m	$⊢ φ \to M \in ℤ$
	ulmcau.s	$⊢ φ \to S \in V$
	ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
Assertion	ulmcau2	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$

Proof

Step	Hyp	Ref	Expression
1		ulmcau.z	$⊢ Z = ℤ_{\geq M}$
2		ulmcau.m	$⊢ φ \to M \in ℤ$
3		ulmcau.s	$⊢ φ \to S \in V$
4		ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
5	1 2 3 4	ulmcau	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
6	1 2 3 4	ulmcaulem	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
7	5 6	bitrd	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$

Metamath Proof Explorer

Theorem ulmcau2

Proof