Loading [MathJax]/jax/output/HTML-CSS/config.js
:: Tietze {E}xtension {T}heorem
:: by Artur Korni{\l}owicz , Grzegorz Bancerek and Adam Naumowicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
theorem
Th1
:
:: TIETZE:1
for
a
,
b
,
c
being
Real
st
|.
(
a
-
b
)
.|
<=
c
holds
(
b
-
c
<=
a
&
a
<=
b
+
c
)
proof
end;
theorem
Th2
:
:: TIETZE:2
for
f
,
g
,
h
being
real-valued
Function
st
f
c=
g
holds
h
-
f
c=
h
-
g
proof
end;
theorem
:: TIETZE:3
for
f
,
g
,
h
being
real-valued
Function
st
f
c=
g
holds
f
-
h
c=
g
-
h
proof
end;
definition
let
f
be
real-valued
Function
;
let
r
be
Real
;
let
X
be
set
;
pred
f
,
X
is_absolutely_bounded_by
r
means
:: TIETZE:def 1
for
x
being
set
st
x
in
X
/\
(
dom
f
)
holds
|.
(
f
.
x
)
.|
<=
r
;
end;
::
deftheorem
defines
is_absolutely_bounded_by
TIETZE:def 1 :
for
f
being
real-valued
Function
for
r
being
Real
for
X
being
set
holds
(
f
,
X
is_absolutely_bounded_by
r
iff for
x
being
set
st
x
in
X
/\
(
dom
f
)
holds
|.
(
f
.
x
)
.|
<=
r
);
registration
cluster
non
empty
Relation-like
NAT
-defined
REAL
-valued
Function-like
constant
total
quasi_total
complex-valued
ext-real-valued
real-valued
summable
convergent
for
Element
of
K10
(
K11
(
NAT
,
REAL
));
existence
ex
b
1
being
Real_Sequence
st
(
b
1
is
summable
&
b
1
is
constant
&
b
1
is
convergent
)
proof
end;
end;
theorem
:: TIETZE:4
for
T1
being
empty
TopSpace
for
T2
being
TopSpace
for
f
being
Function
of
T1
,
T2
holds
f
is
continuous
proof
end;
theorem
:: TIETZE:5
for
f
,
g
being
summable
Real_Sequence
st ( for
n
being
Nat
holds
f
.
n
<=
g
.
n
) holds
Sum
f
<=
Sum
g
proof
end;
theorem
Th6
:
:: TIETZE:6
for
f
being
Real_Sequence
st
f
is
absolutely_summable
holds
|.
(
Sum
f
)
.|
<=
Sum
(
abs
f
)
proof
end;
theorem
Th7
:
:: TIETZE:7
for
f
being
Real_Sequence
for
a
,
r
being
positive
Real
st
r
<
1 & ( for
n
being
Nat
holds
|.
(
(
f
.
n
)
-
(
f
.
(
n
+
1
)
)
)
.|
<=
a
*
(
r
to_power
n
)
) holds
(
f
is
convergent
& ( for
n
being
Nat
holds
|.
(
(
lim
f
)
-
(
f
.
n
)
)
.|
<=
(
a
*
(
r
to_power
n
)
)
/
(
1
-
r
)
) )
proof
end;
theorem
:: TIETZE:8
for
f
being
Real_Sequence
for
a
,
r
being
positive
Real
st
r
<
1 & ( for
n
being
Nat
holds
|.
(
(
f
.
n
)
-
(
f
.
(
n
+
1
)
)
)
.|
<=
a
*
(
r
to_power
n
)
) holds
(
lim
f
>=
(
f
.
0
)
-
(
a
/
(
1
-
r
)
)
&
lim
f
<=
(
f
.
0
)
+
(
a
/
(
1
-
r
)
)
)
proof
end;
theorem
Th9
:
:: TIETZE:9
for
X
,
Z
being non
empty
set
for
F
being
Functional_Sequence
of
X
,
REAL
st
Z
common_on_dom
F
holds
for
a
,
r
being
positive
Real
st
r
<
1 & ( for
n
being
Nat
holds
(
F
.
n
)
-
(
F
.
(
n
+
1
)
)
,
Z
is_absolutely_bounded_by
a
*
(
r
to_power
n
)
) holds
(
F
is_unif_conv_on
Z
& ( for
n
being
Nat
holds
(
lim
(
F
,
Z
)
)
-
(
F
.
n
)
,
Z
is_absolutely_bounded_by
(
a
*
(
r
to_power
n
)
)
/
(
1
-
r
)
) )
proof
end;
theorem
Th10
:
:: TIETZE:10
for
X
,
Z
being non
empty
set
for
F
being
Functional_Sequence
of
X
,
REAL
st
Z
common_on_dom
F
holds
for
a
,
r
being
positive
Real
st
r
<
1 & ( for
n
being
Nat
holds
(
F
.
n
)
-
(
F
.
(
n
+
1
)
)
,
Z
is_absolutely_bounded_by
a
*
(
r
to_power
n
)
) holds
for
z
being
Element
of
Z
holds
(
(
lim
(
F
,
Z
)
)
.
z
>=
(
(
F
.
0
)
.
z
)
-
(
a
/
(
1
-
r
)
)
&
(
lim
(
F
,
Z
)
)
.
z
<=
(
(
F
.
0
)
.
z
)
+
(
a
/
(
1
-
r
)
)
)
proof
end;
theorem
Th11
:
:: TIETZE:11
for
X
,
Z
being non
empty
set
for
F
being
Functional_Sequence
of
X
,
REAL
st
Z
common_on_dom
F
holds
for
a
,
r
being
positive
Real
for
f
being
Function
of
Z
,
REAL
st
r
<
1 & ( for
n
being
Nat
holds
(
F
.
n
)
-
f
,
Z
is_absolutely_bounded_by
a
*
(
r
to_power
n
)
) holds
(
F
is_point_conv_on
Z
&
lim
(
F
,
Z
)
=
f
)
proof
end;
:: Topology
registration
let
T
be
TopSpace
;
let
A
be
closed
Subset
of
T
;
cluster
T
|
A
->
closed
;
coherence
T
|
A
is
closed
by
PRE_TOPC:8
;
end;
theorem
Th12
:
:: TIETZE:12
for
X
,
Y
being non
empty
TopSpace
for
X1
,
X2
being non
empty
SubSpace
of
X
for
f1
being
Function
of
X1
,
Y
for
f2
being
Function
of
X2
,
Y
st (
X1
misses
X2
or
f1
|
(
X1
meet
X2
)
=
f2
|
(
X1
meet
X2
)
) holds
for
x
being
Point
of
X
holds
( (
x
in
the
carrier
of
X1
implies
(
f1
union
f2
)
.
x
=
f1
.
x
) & (
x
in
the
carrier
of
X2
implies
(
f1
union
f2
)
.
x
=
f2
.
x
) )
proof
end;
theorem
Th13
:
:: TIETZE:13
for
X
,
Y
being non
empty
TopSpace
for
X1
,
X2
being non
empty
SubSpace
of
X
for
f1
being
Function
of
X1
,
Y
for
f2
being
Function
of
X2
,
Y
st (
X1
misses
X2
or
f1
|
(
X1
meet
X2
)
=
f2
|
(
X1
meet
X2
)
) holds
rng
(
f1
union
f2
)
c=
(
rng
f1
)
\/
(
rng
f2
)
proof
end;
theorem
Th14
:
:: TIETZE:14
for
X
,
Y
being non
empty
TopSpace
for
X1
,
X2
being non
empty
SubSpace
of
X
for
f1
being
Function
of
X1
,
Y
for
f2
being
Function
of
X2
,
Y
st (
X1
misses
X2
or
f1
|
(
X1
meet
X2
)
=
f2
|
(
X1
meet
X2
)
) holds
( ( for
A
being
Subset
of
X1
holds
(
f1
union
f2
)
.:
A
=
f1
.:
A
) & ( for
A
being
Subset
of
X2
holds
(
f1
union
f2
)
.:
A
=
f2
.:
A
) )
proof
end;
theorem
Th15
:
:: TIETZE:15
for
r
being
Real
for
X
being
set
for
f
,
g
being
real-valued
Function
st
f
c=
g
&
g
,
X
is_absolutely_bounded_by
r
holds
f
,
X
is_absolutely_bounded_by
r
proof
end;
theorem
Th16
:
:: TIETZE:16
for
r
being
Real
for
X
being
set
for
f
,
g
being
real-valued
Function
st (
X
c=
dom
f
or
dom
g
c=
dom
f
) &
f
|
X
=
g
|
X
&
f
,
X
is_absolutely_bounded_by
r
holds
g
,
X
is_absolutely_bounded_by
r
proof
end;
theorem
Th17
:
:: TIETZE:17
for
r
being
Real
for
T
being non
empty
TopSpace
for
A
being
closed
Subset
of
T
st
r
>
0
&
T
is
normal
holds
for
f
being
continuous
Function
of
(
T
|
A
)
,
R^1
st
f
,
A
is_absolutely_bounded_by
r
holds
ex
g
being
continuous
Function
of
T
,
R^1
st
(
g
,
dom
g
is_absolutely_bounded_by
r
/
3 &
f
-
g
,
A
is_absolutely_bounded_by
(
2
*
r
)
/
3 )
proof
end;
:: Urysohn Lemma, simple case
theorem
Th18
:
:: TIETZE:18
for
T
being non
empty
TopSpace
st ( for
A
,
B
being non
empty
closed
Subset
of
T
st
A
misses
B
holds
ex
f
being
continuous
Function
of
T
,
R^1
st
(
f
.:
A
=
{
0
}
&
f
.:
B
=
{
1
}
) ) holds
T
is
normal
proof
end;
theorem
Th19
:
:: TIETZE:19
for
T
being non
empty
TopSpace
for
f
being
Function
of
T
,
R^1
for
x
being
Point
of
T
holds
(
f
is_continuous_at
x
iff for
e
being
Real
st
e
>
0
holds
ex
H
being
Subset
of
T
st
(
H
is
open
&
x
in
H
& ( for
y
being
Point
of
T
st
y
in
H
holds
|.
(
(
f
.
y
)
-
(
f
.
x
)
)
.|
<
e
) ) )
proof
end;
theorem
Th20
:
:: TIETZE:20
for
T
being non
empty
TopSpace
for
F
being
Functional_Sequence
of the
carrier
of
T
,
REAL
st
F
is_unif_conv_on
the
carrier
of
T
& ( for
i
being
Nat
holds
F
.
i
is
continuous
Function
of
T
,
R^1
) holds
lim
(
F
, the
carrier
of
T
) is
continuous
Function
of
T
,
R^1
proof
end;
theorem
Th21
:
:: TIETZE:21
for
T
being non
empty
TopSpace
for
f
being
Function
of
T
,
R^1
for
r
being
positive
Real
holds
(
f
, the
carrier
of
T
is_absolutely_bounded_by
r
iff
f
is
Function
of
T
,
(
Closed-Interval-TSpace
(
(
-
r
)
,
r
)
)
)
proof
end;
theorem
Th22
:
:: TIETZE:22
for
r
being
Real
for
X
being
set
for
f
,
g
being
real-valued
Function
st
f
-
g
,
X
is_absolutely_bounded_by
r
holds
g
-
f
,
X
is_absolutely_bounded_by
r
proof
end;
:: Tietze Extension Theorem
::
Tietze extension theorem
theorem
:: TIETZE:23
for
T
being non
empty
TopSpace
st
T
is
normal
holds
for
A
being
closed
Subset
of
T
for
f
being
Function
of
(
T
|
A
)
,
(
Closed-Interval-TSpace
(
(
-
1
)
,1)
)
st
f
is
continuous
holds
ex
g
being
continuous
Function
of
T
,
(
Closed-Interval-TSpace
(
(
-
1
)
,1)
)
st
g
|
A
=
f
proof
end;
theorem
:: TIETZE:24
for
T
being non
empty
TopSpace
st ( for
A
being non
empty
closed
Subset
of
T
for
f
being
continuous
Function
of
(
T
|
A
)
,
(
Closed-Interval-TSpace
(
(
-
1
)
,1)
)
ex
g
being
continuous
Function
of
T
,
(
Closed-Interval-TSpace
(
(
-
1
)
,1)
)
st
g
|
A
=
f
) holds
T
is
normal
proof
end;