This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmrel

Description: The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015)

		Ref	Expression
	Assertion	ulmrel	$⊢ Rel \underset{u}{⇝} (S)$

Step	Hyp	Ref	Expression
1		df-ulm	$⊢ \underset{u}{⇝} = (s \in V ⟼ \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{s} \land y : s ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x)\})$
2	1	relmptopab	$⊢ Rel \underset{u}{⇝} (S)$