Database
BASIC REAL AND COMPLEX FUNCTIONS
Sequences and series
Uniform convergence
ulmrel
Next ⟩
ulmscl
Metamath Proof Explorer
Ascii
Unicode
Theorem
ulmrel
Description:
The uniform limit relation is a relation.
(Contributed by
Mario Carneiro
, 26-Feb-2015)
Ref
Expression
Assertion
ulmrel
⊢
Rel
⁡
⇝
u
⁡
S
Proof
Step
Hyp
Ref
Expression
1
df-ulm
⊢
⇝
u
=
s
∈
V
⟼
f
y
|
∃
n
∈
ℤ
f
:
ℤ
≥
n
⟶
ℂ
s
∧
y
:
s
⟶
ℂ
∧
∀
x
∈
ℝ
+
∃
j
∈
ℤ
≥
n
∀
k
∈
ℤ
≥
j
∀
z
∈
s
f
⁡
k
⁡
z
−
y
⁡
z
<
x
2
1
relmptopab
⊢
Rel
⁡
⇝
u
⁡
S