Loading [MathJax]/extensions/tex2jax.js
:: Ascoli-Arzela's Theorem
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
definition
let
X
be non
empty
MetrSpace
;
let
Y
be
Subset
of
X
;
func
Cl
Y
->
Subset
of
X
means
:
Def1
:
:: ASCOLI:def 1
ex
Z
being
Subset
of
(
TopSpaceMetr
X
)
st
(
Z
=
Y
&
it
=
Cl
Z
);
correctness
existence
ex
b
1
being
Subset
of
X
ex
Z
being
Subset
of
(
TopSpaceMetr
X
)
st
(
Z
=
Y
&
b
1
=
Cl
Z
)
;
uniqueness
for
b
1
,
b
2
being
Subset
of
X
st ex
Z
being
Subset
of
(
TopSpaceMetr
X
)
st
(
Z
=
Y
&
b
1
=
Cl
Z
) & ex
Z
being
Subset
of
(
TopSpaceMetr
X
)
st
(
Z
=
Y
&
b
2
=
Cl
Z
) holds
b
1
=
b
2
;
proof
end;
end;
::
deftheorem
Def1
defines
Cl
ASCOLI:def 1 :
for
X
being non
empty
MetrSpace
for
Y
,
b
3
being
Subset
of
X
holds
(
b
3
=
Cl
Y
iff ex
Z
being
Subset
of
(
TopSpaceMetr
X
)
st
(
Z
=
Y
&
b
3
=
Cl
Z
) );
theorem
Th1
:
:: ASCOLI:1
for
X
being
RealNormSpace
for
Y
being
Subset
of
X
for
Z
being
Subset
of
(
MetricSpaceNorm
X
)
st
Y
=
Z
holds
Cl
Y
=
Cl
Z
proof
end;
registration
let
X
be non
empty
MetrSpace
;
let
H
be non
empty
Subset
of
X
;
cluster
Cl
H
->
non
empty
;
correctness
coherence
not
Cl
H
is
empty
;
proof
end;
end;
theorem
Th2
:
:: ASCOLI:2
for
S
being
TopSpace
for
F
being
FinSequence
of
bool
the
carrier
of
S
st ( for
i
being
Nat
st
i
in
Seg
(
len
F
)
holds
F
/.
i
is
compact
) holds
union
(
rng
F
)
is
compact
proof
end;
theorem
Th3
:
:: ASCOLI:3
for
S
being non
empty
TopSpace
for
T
being
NormedLinearTopSpace
for
f
being
Function
of
S
,
T
for
x
being
Point
of
S
holds
(
f
is_continuous_at
x
iff for
e
being
Real
st
0
<
e
holds
ex
H
being
Subset
of
S
st
(
H
is
open
&
x
in
H
& ( for
y
being
Point
of
S
st
y
in
H
holds
||.
(
(
f
.
x
)
-
(
f
.
y
)
)
.||
<
e
) ) )
proof
end;
theorem
Th4
:
:: ASCOLI:4
for
S
being non
empty
MetrSpace
for
V
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
f
being
Function
of
V
,
T
st
V
=
TopSpaceMetr
S
holds
(
f
is
continuous
iff for
e
being
Real
st
0
<
e
holds
ex
d
being
Real
st
(
0
<
d
& ( for
x1
,
x2
being
Point
of
S
st
dist
(
x1
,
x2
)
<
d
holds
||.
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
.||
<
e
) ) )
proof
end;
definition
let
S
be non
empty
MetrSpace
;
let
T
be
RealNormSpace
;
let
F
be
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
;
attr
F
is
equibounded
means
:: ASCOLI:def 2
ex
K
being
Real
st
for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x
being
Element
of
S
holds
||.
(
f
.
x
)
.||
<=
K
;
end;
::
deftheorem
defines
equibounded
ASCOLI:def 2 :
for
S
being non
empty
MetrSpace
for
T
being
RealNormSpace
for
F
being
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
holds
(
F
is
equibounded
iff ex
K
being
Real
st
for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x
being
Element
of
S
holds
||.
(
f
.
x
)
.||
<=
K
);
definition
let
S
be non
empty
MetrSpace
;
let
T
be
RealNormSpace
;
let
F
be
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
;
let
x0
be
Point
of
S
;
pred
F
is_equicontinuous_at
x0
means
:: ASCOLI:def 3
for
e
being
Real
st
0
<
e
holds
ex
d
being
Real
st
(
0
<
d
& ( for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x
being
Point
of
S
st
dist
(
x
,
x0
)
<
d
holds
||.
(
(
f
.
x
)
-
(
f
.
x0
)
)
.||
<
e
) );
end;
::
deftheorem
defines
is_equicontinuous_at
ASCOLI:def 3 :
for
S
being non
empty
MetrSpace
for
T
being
RealNormSpace
for
F
being
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
for
x0
being
Point
of
S
holds
(
F
is_equicontinuous_at
x0
iff for
e
being
Real
st
0
<
e
holds
ex
d
being
Real
st
(
0
<
d
& ( for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x
being
Point
of
S
st
dist
(
x
,
x0
)
<
d
holds
||.
(
(
f
.
x
)
-
(
f
.
x0
)
)
.||
<
e
) ) );
definition
let
S
be non
empty
MetrSpace
;
let
T
be
RealNormSpace
;
let
F
be
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
;
attr
F
is
equicontinuous
means
:: ASCOLI:def 4
for
e
being
Real
st
0
<
e
holds
ex
d
being
Real
st
(
0
<
d
& ( for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x1
,
x2
being
Point
of
S
st
dist
(
x1
,
x2
)
<
d
holds
||.
(
(
f
.
x1
)
-
(
f
.
x2
)
)
.||
<
e
) );
end;
::
deftheorem
defines
equicontinuous
ASCOLI:def 4 :
for
S
being non
empty
MetrSpace
for
T
being
RealNormSpace
for
F
being
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
holds
(
F
is
equicontinuous
iff for
e
being
Real
st
0
<
e
holds
ex
d
being
Real
st
(
0
<
d
& ( for
f
being
Function
of the
carrier
of
S
, the
carrier
of
T
st
f
in
F
holds
for
x1
,
x2
being
Point
of
S
st
dist
(
x1
,
x2
)
<
d
holds
||.
(
(
f
.
x1
)
-
(
f
.
x2
)
)
.||
<
e
) ) );
theorem
Th5
:
:: ASCOLI:5
for
S
being non
empty
MetrSpace
for
T
being
RealNormSpace
for
F
being
Subset
of
(
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
)
st
TopSpaceMetr
S
is
compact
holds
(
F
is
equicontinuous
iff for
x
being
Point
of
S
holds
F
is_equicontinuous_at
x
)
proof
end;
theorem
Th6
:
:: ASCOLI:6
for
Z
being
RealNormSpace
holds
(
Z
is
complete
iff
MetricSpaceNorm
Z
is
complete
)
proof
end;
theorem
Th7
:
:: ASCOLI:7
for
Z
being
RealNormSpace
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
Z
)
st
Z
is
complete
holds
(
MetricSpaceNorm
Z
)
|
(
Cl
H
)
is
complete
proof
end;
theorem
Th8
:
:: ASCOLI:8
for
Z
being
RealNormSpace
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
Z
)
holds
(
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
iff
(
MetricSpaceNorm
Z
)
|
(
Cl
H
)
is
totally_bounded
)
proof
end;
theorem
Th9
:
:: ASCOLI:9
for
Z
being
RealNormSpace
for
F
being non
empty
Subset
of
Z
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
Z
)
st
Z
is
complete
&
H
=
F
&
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
holds
(
Cl
H
is
sequentially_compact
&
(
MetricSpaceNorm
Z
)
|
(
Cl
H
)
is
compact
&
Cl
F
is
compact
)
proof
end;
theorem
:: ASCOLI:10
for
Z
being
RealNormSpace
for
F
being non
empty
Subset
of
Z
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
Z
)
for
T
being
Subset
of
(
TopSpaceNorm
Z
)
st
Z
is
complete
&
H
=
F
&
H
=
T
holds
( (
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
implies
Cl
H
is
sequentially_compact
) & (
Cl
H
is
sequentially_compact
implies
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
) & (
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
implies
(
MetricSpaceNorm
Z
)
|
(
Cl
H
)
is
compact
) & (
(
MetricSpaceNorm
Z
)
|
(
Cl
H
)
is
compact
implies
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
) & (
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
implies
Cl
F
is
compact
) & (
Cl
F
is
compact
implies
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
) & (
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
implies
Cl
T
is
compact
) & (
Cl
T
is
compact
implies
(
MetricSpaceNorm
Z
)
|
H
is
totally_bounded
) )
proof
end;
theorem
Th11
:
:: ASCOLI:11
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
st
T
is
complete
holds
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
holds
(
Cl
H
is
sequentially_compact
iff
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
|
H
is
totally_bounded
)
proof
end;
theorem
Th12
:
:: ASCOLI:12
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
st
T
is
complete
holds
for
F
being non
empty
Subset
of
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
st
H
=
F
holds
(
Cl
F
is
compact
iff
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
|
H
is
totally_bounded
)
proof
end;
theorem
Th13
:
:: ASCOLI:13
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
st
S
=
TopSpaceMetr
M
&
T
is
complete
holds
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
st
G
=
H
&
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
|
H
is
totally_bounded
holds
(
G
is
equibounded
&
G
is
equicontinuous
)
proof
end;
theorem
Th14
:
:: ASCOLI:14
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
st
S
=
TopSpaceMetr
M
&
T
is
complete
holds
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
st
G
=
H
&
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
|
H
is
totally_bounded
holds
( ( for
x
being
Point
of
S
for
Hx
being non
empty
Subset
of
(
MetricSpaceNorm
T
)
st
Hx
=
{
(
f
.
x
)
where
f
is
Function
of
S
,
T
:
f
in
H
}
holds
(
MetricSpaceNorm
T
)
|
Hx
is
totally_bounded
) &
G
is
equicontinuous
)
proof
end;
theorem
Th15
:
:: ASCOLI:15
for
T
being
NormedLinearTopSpace
for
RNS
being
RealNormSpace
st
RNS
=
NORMSTR
(# the
carrier
of
T
, the
ZeroF
of
T
, the
U5
of
T
, the
U7
of
T
, the
normF
of
T
#) & the
topology
of
T
=
the
topology
of
(
TopSpaceNorm
RNS
)
holds
(
distance_by_norm_of
RNS
=
distance_by_norm_of
T
&
MetricSpaceNorm
RNS
=
MetricSpaceNorm
T
&
TopSpaceNorm
T
=
TopSpaceNorm
RNS
)
proof
end;
theorem
Th16
:
:: ASCOLI:16
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
st
S
=
TopSpaceMetr
M
&
T
is
complete
&
G
=
H
holds
(
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
|
H
is
totally_bounded
iff (
G
is
equicontinuous
& ( for
x
being
Point
of
S
for
Hx
being non
empty
Subset
of
(
MetricSpaceNorm
T
)
st
Hx
=
{
(
f
.
x
)
where
f
is
Function
of
S
,
T
:
f
in
H
}
holds
(
MetricSpaceNorm
T
)
|
(
Cl
Hx
)
is
compact
) ) )
proof
end;
theorem
:: ASCOLI:17
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
for
H
being non
empty
Subset
of
(
MetricSpaceNorm
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
)
st
S
=
TopSpaceMetr
M
&
T
is
complete
&
G
=
H
holds
(
Cl
H
is
sequentially_compact
iff (
G
is
equicontinuous
& ( for
x
being
Point
of
S
for
Hx
being non
empty
Subset
of
(
MetricSpaceNorm
T
)
st
Hx
=
{
(
f
.
x
)
where
f
is
Function
of
S
,
T
:
f
in
H
}
holds
(
MetricSpaceNorm
T
)
|
(
Cl
Hx
)
is
compact
) ) )
proof
end;
theorem
Th18
:
:: ASCOLI:18
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
F
being non
empty
Subset
of
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
st
S
=
TopSpaceMetr
M
&
T
is
complete
&
G
=
F
holds
(
Cl
F
is
compact
iff (
G
is
equicontinuous
& ( for
x
being
Point
of
S
for
Fx
being non
empty
Subset
of
(
MetricSpaceNorm
T
)
st
Fx
=
{
(
f
.
x
)
where
f
is
Function
of
S
,
T
:
f
in
F
}
holds
(
MetricSpaceNorm
T
)
|
(
Cl
Fx
)
is
compact
) ) )
proof
end;
theorem
:: ASCOLI:19
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
F
being non
empty
Subset
of
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
st
S
=
TopSpaceMetr
M
&
T
is
complete
&
G
=
F
holds
(
Cl
F
is
compact
iff ( ( for
x
being
Point
of
M
holds
G
is_equicontinuous_at
x
) & ( for
x
being
Point
of
S
for
Fx
being non
empty
Subset
of
(
MetricSpaceNorm
T
)
st
Fx
=
{
(
f
.
x
)
where
f
is
Function
of
S
,
T
:
f
in
F
}
holds
(
MetricSpaceNorm
T
)
|
(
Cl
Fx
)
is
compact
) ) )
proof
end;
theorem
Th20
:
:: ASCOLI:20
for
T
being
NormedLinearTopSpace
holds
(
T
is
compact
iff
TopSpaceNorm
T
is
compact
)
proof
end;
theorem
Th21
:
:: ASCOLI:21
for
T
being
NormedLinearTopSpace
for
X
being
set
holds
(
X
is
compact
Subset
of
T
iff
X
is
compact
Subset
of
(
TopSpaceNorm
T
)
)
proof
end;
theorem
ThLast
:
:: ASCOLI:22
for
T
being
NormedLinearTopSpace
st
T
is
compact
holds
T
is
complete
proof
end;
registration
cluster
non
empty
V70
()
V95
()
V96
()
V97
()
V98
()
V99
()
V100
()
V101
()
discerning
V106
()
RealNormSpace-like
TopSpace-like
T_2
V213
()
V214
()
compact
strict
norm-generated
->
complete
for
RLNormTopStruct
;
coherence
for
b
1
being
NormedLinearTopSpace
st
b
1
is
compact
holds
b
1
is
complete
by
ThLast
;
end;
theorem
:: ASCOLI:23
for
M
being non
empty
MetrSpace
for
S
being non
empty
compact
TopSpace
for
T
being
NormedLinearTopSpace
for
U
being
compact
Subset
of
T
for
F
being non
empty
Subset
of
(
R_NormSpace_of_ContinuousFunctions
(
S
,
T
)
)
for
G
being
Subset
of
(
Funcs
( the
carrier
of
M
, the
carrier
of
T
)
)
st
S
=
TopSpaceMetr
M
&
T
is
complete
&
G
=
F
& ( for
f
being
Function
st
f
in
F
holds
rng
f
c=
U
) holds
( (
Cl
F
is
compact
implies (
G
is
equibounded
&
G
is
equicontinuous
) ) & (
G
is
equicontinuous
implies
Cl
F
is
compact
) )
proof
end;