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

Metamath Proof Explorer

Theorem climrel

Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	climrel	$⊢ Rel ⇝$

Step	Hyp	Ref	Expression
1		df-clim	$⊢ ⇝ = \{⟨f, y⟩ \| (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))\}$
2	1	relopabiv	$⊢ Rel ⇝$