:: Real Function Continuity
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
let
x0
be
real
number
;
pred
f
is_continuous_in
x0
means
:
Def1
:
:: FCONT_1:def 1
for
s1
being
Real_Sequence
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
.
x0
=
lim
(
f
/*
s1
)
);
end;
::
deftheorem
Def1
defines
is_continuous_in
FCONT_1:def 1 :
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
holds
(
f
is_continuous_in
x0
iff for
s1
being
Real_Sequence
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
.
x0
=
lim
(
f
/*
s1
)
) );
theorem
Th1
:
:: FCONT_1:1
for
X
being
set
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st
x0
in
X
&
f
is_continuous_in
x0
holds
f
|
X
is_continuous_in
x0
proof
end;
theorem
:: FCONT_1:2
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is_continuous_in
x0
iff for
s1
being
Real_Sequence
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
& ( for
n
being
Element
of
NAT
holds
s1
.
n
<>
x0
) holds
(
f
/*
s1
is
convergent
&
f
.
x0
=
lim
(
f
/*
s1
)
) )
proof
end;
theorem
Th3
:
:: FCONT_1:3
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is_continuous_in
x0
iff for
r
being
real
number
st
0
<
r
holds
ex
s
being
real
number
st
(
0
<
s
& ( for
x1
being
real
number
st
x1
in
dom
f
&
abs
(
x1
-
x0
)
<
s
holds
abs
(
(
f
.
x1
)
-
(
f
.
x0
)
)
<
r
) ) )
proof
end;
theorem
Th4
:
:: FCONT_1:4
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
holds
(
f
is_continuous_in
x0
iff for
N1
being
Neighbourhood
of
f
.
x0
ex
N
being
Neighbourhood
of
x0
st
for
x1
being
real
number
st
x1
in
dom
f
&
x1
in
N
holds
f
.
x1
in
N1
)
proof
end;
theorem
Th5
:
:: FCONT_1:5
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
holds
(
f
is_continuous_in
x0
iff for
N1
being
Neighbourhood
of
f
.
x0
ex
N
being
Neighbourhood
of
x0
st
f
.:
N
c=
N1
)
proof
end;
theorem
:: FCONT_1:6
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st ex
N
being
Neighbourhood
of
x0
st
(
dom
f
)
/\
N
=
{
x0
}
holds
f
is_continuous_in
x0
proof
end;
theorem
Th7
:
:: FCONT_1:7
for
x0
being
real
number
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
x0
in
(
dom
f1
)
/\
(
dom
f2
)
&
f1
is_continuous_in
x0
&
f2
is_continuous_in
x0
holds
(
f1
+
f2
is_continuous_in
x0
&
f1
-
f2
is_continuous_in
x0
&
f1
(#)
f2
is_continuous_in
x0
)
proof
end;
theorem
Th8
:
:: FCONT_1:8
for
x0
,
r
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st
x0
in
dom
f
&
f
is_continuous_in
x0
holds
r
(#)
f
is_continuous_in
x0
proof
end;
theorem
:: FCONT_1:9
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st
x0
in
dom
f
&
f
is_continuous_in
x0
holds
(
abs
f
is_continuous_in
x0
&
-
f
is_continuous_in
x0
)
proof
end;
theorem
Th10
:
:: FCONT_1:10
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_continuous_in
x0
&
f
.
x0
<>
0
holds
f
^
is_continuous_in
x0
proof
end;
theorem
:: FCONT_1:11
for
x0
being
real
number
for
f2
,
f1
being
PartFunc
of
REAL
,
REAL
st
x0
in
dom
f2
&
f1
is_continuous_in
x0
&
f1
.
x0
<>
0
&
f2
is_continuous_in
x0
holds
f2
/
f1
is_continuous_in
x0
proof
end;
theorem
Th12
:
:: FCONT_1:12
for
x0
being
real
number
for
f2
,
f1
being
PartFunc
of
REAL
,
REAL
st
x0
in
dom
(
f2
*
f1
)
&
f1
is_continuous_in
x0
&
f2
is_continuous_in
f1
.
x0
holds
f2
*
f1
is_continuous_in
x0
proof
end;
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
attr
f
is
continuous
means
:
Def2
:
:: FCONT_1:def 2
for
x0
being
real
number
st
x0
in
dom
f
holds
f
is_continuous_in
x0
;
end;
::
deftheorem
Def2
defines
continuous
FCONT_1:def 2 :
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is
continuous
iff for
x0
being
real
number
st
x0
in
dom
f
holds
f
is_continuous_in
x0
);
theorem
Th13
:
:: FCONT_1:13
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f
holds
(
f
|
X
is
continuous
iff for
s1
being
Real_Sequence
st
rng
s1
c=
X
&
s1
is
convergent
&
lim
s1
in
X
holds
(
f
/*
s1
is
convergent
&
f
.
(
lim
s1
)
=
lim
(
f
/*
s1
)
) )
proof
end;
theorem
Th14
:
:: FCONT_1:14
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f
holds
(
f
|
X
is
continuous
iff for
x0
,
r
being
real
number
st
x0
in
X
&
0
<
r
holds
ex
s
being
real
number
st
(
0
<
s
& ( for
x1
being
real
number
st
x1
in
X
&
abs
(
x1
-
x0
)
<
s
holds
abs
(
(
f
.
x1
)
-
(
f
.
x0
)
)
<
r
) ) )
proof
end;
registration
cluster
Function-like
V8
()
->
continuous
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
V8
() holds
b
1
is
continuous
proof
end;
end;
registration
cluster
Relation-like
REAL
-defined
REAL
-valued
Function-like
complex-valued
ext-real-valued
real-valued
continuous
for
Element
of
bool
[:
REAL
,
REAL
:]
;
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
continuous
proof
end;
end;
registration
let
f
be
continuous
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
cluster
f
|
X
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f
|
X
holds
b
1
is
continuous
proof
end;
end;
theorem
:: FCONT_1:15
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
|
X
is
continuous
iff
(
f
|
X
)
|
X
is
continuous
) ;
theorem
Th16
:
:: FCONT_1:16
for
X
,
X1
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
continuous
&
X1
c=
X
holds
f
|
X1
is
continuous
proof
end;
registration
cluster
Function-like
empty
->
continuous
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
empty
holds
b
1
is
continuous
;
end;
registration
let
f
be
PartFunc
of
REAL
,
REAL
;
let
X
be
trivial
set
;
cluster
f
|
X
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f
|
X
holds
b
1
is
continuous
proof
end;
end;
theorem
:: FCONT_1:17
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
holds
f
|
{
x0
}
is
continuous
;
registration
let
f1
,
f2
be
continuous
PartFunc
of
REAL
,
REAL
;
cluster
f1
+
f2
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
+
f2
holds
b
1
is
continuous
proof
end;
cluster
f1
-
f2
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
-
f2
holds
b
1
is
continuous
proof
end;
cluster
f1
(#)
f2
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
(#)
f2
holds
b
1
is
continuous
proof
end;
end;
theorem
Th18
:
:: FCONT_1:18
for
X
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
X
c=
(
dom
f1
)
/\
(
dom
f2
)
&
f1
|
X
is
continuous
&
f2
|
X
is
continuous
holds
(
(
f1
+
f2
)
|
X
is
continuous
&
(
f1
-
f2
)
|
X
is
continuous
&
(
f1
(#)
f2
)
|
X
is
continuous
)
proof
end;
theorem
:: FCONT_1:19
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f1
&
X1
c=
dom
f2
&
f1
|
X
is
continuous
&
f2
|
X1
is
continuous
holds
(
(
f1
+
f2
)
|
(
X
/\
X1
)
is
continuous
&
(
f1
-
f2
)
|
(
X
/\
X1
)
is
continuous
&
(
f1
(#)
f2
)
|
(
X
/\
X1
)
is
continuous
)
proof
end;
registration
let
f
be
continuous
PartFunc
of
REAL
,
REAL
;
let
r
be
real
number
;
cluster
r
(#)
f
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
r
(#)
f
holds
b
1
is
continuous
proof
end;
end;
theorem
Th20
:
:: FCONT_1:20
for
r
being
real
number
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f
&
f
|
X
is
continuous
holds
(
r
(#)
f
)
|
X
is
continuous
proof
end;
theorem
:: FCONT_1:21
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f
&
f
|
X
is
continuous
holds
(
(
abs
f
)
|
X
is
continuous
&
(
-
f
)
|
X
is
continuous
)
proof
end;
theorem
Th22
:
:: FCONT_1:22
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
continuous
&
f
"
{
0
}
=
{}
holds
(
f
^
)
|
X
is
continuous
proof
end;
theorem
:: FCONT_1:23
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
continuous
&
(
f
|
X
)
"
{
0
}
=
{}
holds
(
f
^
)
|
X
is
continuous
proof
end;
theorem
:: FCONT_1:24
for
X
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
X
c=
(
dom
f1
)
/\
(
dom
f2
)
&
f1
|
X
is
continuous
&
f1
"
{
0
}
=
{}
&
f2
|
X
is
continuous
holds
(
f2
/
f1
)
|
X
is
continuous
proof
end;
registration
let
f1
,
f2
be
continuous
PartFunc
of
REAL
,
REAL
;
cluster
f1
(#)
f2
->
continuous
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f2
*
f1
holds
b
1
is
continuous
proof
end;
end;
theorem
:: FCONT_1:25
for
X
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
|
X
is
continuous
&
f2
|
(
f1
.:
X
)
is
continuous
holds
(
f2
*
f1
)
|
X
is
continuous
proof
end;
theorem
:: FCONT_1:26
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
|
X
is
continuous
&
f2
|
X1
is
continuous
holds
(
f2
*
f1
)
|
(
X
/\
(
f1
"
X1
)
)
is
continuous
proof
end;
theorem
:: FCONT_1:27
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is
total
& ( for
x1
,
x2
being
real
number
holds
f
.
(
x1
+
x2
)
=
(
f
.
x1
)
+
(
f
.
x2
)
) & ex
x0
being
real
number
st
f
is_continuous_in
x0
holds
f
|
REAL
is
continuous
proof
end;
theorem
Th28
:
:: FCONT_1:28
for
f
being
PartFunc
of
REAL
,
REAL
st
dom
f
is
compact
&
f
|
(
dom
f
)
is
continuous
holds
rng
f
is
compact
proof
end;
theorem
:: FCONT_1:29
for
Y
being
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Y
c=
dom
f
&
Y
is
compact
&
f
|
Y
is
continuous
holds
f
.:
Y
is
compact
proof
end;
theorem
Th30
:
:: FCONT_1:30
for
f
being
PartFunc
of
REAL
,
REAL
st
dom
f
<>
{}
&
dom
f
is
compact
&
f
|
(
dom
f
)
is
continuous
holds
ex
x1
,
x2
being
real
number
st
(
x1
in
dom
f
&
x2
in
dom
f
&
f
.
x1
=
upper_bound
(
rng
f
)
&
f
.
x2
=
lower_bound
(
rng
f
)
)
proof
end;
::
Weierstrass Extreme Value Theorem
theorem
:: FCONT_1:31
for
f
being
PartFunc
of
REAL
,
REAL
for
Y
being
Subset
of
REAL
st
Y
<>
{}
&
Y
c=
dom
f
&
Y
is
compact
&
f
|
Y
is
continuous
holds
ex
x1
,
x2
being
real
number
st
(
x1
in
Y
&
x2
in
Y
&
f
.
x1
=
upper_bound
(
f
.:
Y
)
&
f
.
x2
=
lower_bound
(
f
.:
Y
)
)
proof
end;
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
attr
f
is
Lipschitzian
means
:
Def3
:
:: FCONT_1:def 3
ex
r
being
real
number
st
(
0
<
r
& ( for
x1
,
x2
being
real
number
st
x1
in
dom
f
&
x2
in
dom
f
holds
abs
(
(
f
.
x1
)
-
(
f
.
x2
)
)
<=
r
*
(
abs
(
x1
-
x2
)
)
) );
end;
::
deftheorem
Def3
defines
Lipschitzian
FCONT_1:def 3 :
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is
Lipschitzian
iff ex
r
being
real
number
st
(
0
<
r
& ( for
x1
,
x2
being
real
number
st
x1
in
dom
f
&
x2
in
dom
f
holds
abs
(
(
f
.
x1
)
-
(
f
.
x2
)
)
<=
r
*
(
abs
(
x1
-
x2
)
)
) ) );
theorem
Th32
:
:: FCONT_1:32
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
|
X
is
Lipschitzian
iff ex
r
being
real
number
st
(
0
<
r
& ( for
x1
,
x2
being
real
number
st
x1
in
dom
(
f
|
X
)
&
x2
in
dom
(
f
|
X
)
holds
abs
(
(
f
.
x1
)
-
(
f
.
x2
)
)
<=
r
*
(
abs
(
x1
-
x2
)
)
) ) )
proof
end;
registration
cluster
Function-like
empty
->
Lipschitzian
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
empty
holds
b
1
is
Lipschitzian
proof
end;
end;
registration
cluster
Relation-like
REAL
-defined
REAL
-valued
Function-like
empty
complex-valued
ext-real-valued
real-valued
for
Element
of
bool
[:
REAL
,
REAL
:]
;
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
empty
proof
end;
end;
registration
let
f
be
Lipschitzian
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
cluster
f
|
X
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f
|
X
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: FCONT_1:33
for
X
,
X1
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
Lipschitzian
&
X1
c=
X
holds
f
|
X1
is
Lipschitzian
proof
end;
registration
let
f1
,
f2
be
Lipschitzian
PartFunc
of
REAL
,
REAL
;
cluster
f1
+
f2
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
+
f2
holds
b
1
is
Lipschitzian
proof
end;
cluster
f1
-
f2
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
-
f2
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: FCONT_1:34
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
|
X
is
Lipschitzian
&
f2
|
X1
is
Lipschitzian
holds
(
f1
+
f2
)
|
(
X
/\
X1
)
is
Lipschitzian
proof
end;
theorem
:: FCONT_1:35
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
|
X
is
Lipschitzian
&
f2
|
X1
is
Lipschitzian
holds
(
f1
-
f2
)
|
(
X
/\
X1
)
is
Lipschitzian
proof
end;
registration
let
f1
,
f2
be
bounded
Lipschitzian
PartFunc
of
REAL
,
REAL
;
cluster
f1
(#)
f2
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
f1
(#)
f2
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: FCONT_1:36
for
X
,
X1
,
Z
,
Z1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
|
X
is
Lipschitzian
&
f2
|
X1
is
Lipschitzian
&
f1
|
Z
is
bounded
&
f2
|
Z1
is
bounded
holds
(
f1
(#)
f2
)
|
(
(
(
X
/\
Z
)
/\
X1
)
/\
Z1
)
is
Lipschitzian
proof
end;
registration
let
f
be
Lipschitzian
PartFunc
of
REAL
,
REAL
;
let
p
be
real
number
;
cluster
p
(#)
f
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
p
(#)
f
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: FCONT_1:37
for
X
being
set
for
p
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
Lipschitzian
&
X
c=
dom
f
holds
(
p
(#)
f
)
|
X
is
Lipschitzian
proof
end;
registration
let
f
be
Lipschitzian
PartFunc
of
REAL
,
REAL
;
cluster
|.
f
.|
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
abs
f
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: FCONT_1:38
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
Lipschitzian
holds
(
-
(
f
|
X
)
is
Lipschitzian
&
(
abs
f
)
|
X
is
Lipschitzian
)
proof
end;
registration
cluster
Function-like
V8
()
->
Lipschitzian
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
V8
() holds
b
1
is
Lipschitzian
proof
end;
end;
registration
let
Y
be
Subset
of
REAL
;
cluster
id
Y
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
id
Y
holds
b
1
is
Lipschitzian
proof
end;
end;
registration
cluster
Function-like
Lipschitzian
->
continuous
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
Lipschitzian
holds
b
1
is
continuous
proof
end;
end;
theorem
:: FCONT_1:39
for
f
being
PartFunc
of
REAL
,
REAL
st ex
r
being
real
number
st
rng
f
=
{
r
}
holds
f
is
continuous
proof
end;
theorem
:: FCONT_1:40
for
f
being
PartFunc
of
REAL
,
REAL
st ( for
x0
being
real
number
st
x0
in
dom
f
holds
f
.
x0
=
x0
) holds
f
is
continuous
proof
end;
theorem
Th41
:
:: FCONT_1:41
for
X
being
set
for
r
,
p
being
real
number
for
f
being
PartFunc
of
REAL
,
REAL
st ( for
x0
being
real
number
st
x0
in
X
holds
f
.
x0
=
(
r
*
x0
)
+
p
) holds
f
|
X
is
continuous
proof
end;
theorem
Th42
:
:: FCONT_1:42
for
f
being
PartFunc
of
REAL
,
REAL
st ( for
x0
being
real
number
st
x0
in
dom
f
holds
f
.
x0
=
x0
^2
) holds
f
|
(
dom
f
)
is
continuous
proof
end;
theorem
:: FCONT_1:43
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
X
c=
dom
f
& ( for
x0
being
real
number
st
x0
in
X
holds
f
.
x0
=
x0
^2
) holds
f
|
X
is
continuous
proof
end;
theorem
Th44
:
:: FCONT_1:44
for
f
being
PartFunc
of
REAL
,
REAL
st ( for
x0
being
real
number
st
x0
in
dom
f
holds
f
.
x0
=
abs
x0
) holds
f
is
continuous
proof
end;
theorem
:: FCONT_1:45
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st ( for
x0
being
real
number
st
x0
in
X
holds
f
.
x0
=
abs
x0
) holds
f
|
X
is
continuous
proof
end;
theorem
Th46
:
:: FCONT_1:46
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
|
X
is
monotone
& ex
p
,
g
being
real
number
st
(
p
<=
g
&
f
.:
X
=
[.
p
,
g
.]
) holds
f
|
X
is
continuous
proof
end;
theorem
:: FCONT_1:47
for
p
,
g
being
real
number
for
f
being
one-to-one
PartFunc
of
REAL
,
REAL
st
p
<=
g
&
[.
p
,
g
.]
c=
dom
f
& (
f
|
[.
p
,
g
.]
is
increasing
or
f
|
[.
p
,
g
.]
is
decreasing
) holds
(
(
f
|
[.
p
,
g
.]
)
"
)
|
(
f
.:
[.
p
,
g
.]
)
is
continuous
proof
end;
:: from
definition
let
a
,
b
be
real
number
;
func
AffineMap
(
a
,
b
)
->
Function
of
REAL
,
REAL
means
:
Def4
:
:: FCONT_1:def 4
for
x
being
real
number
holds
it
.
x
=
(
a
*
x
)
+
b
;
existence
ex
b
1
being
Function
of
REAL
,
REAL
st
for
x
being
real
number
holds
b
1
.
x
=
(
a
*
x
)
+
b
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of
REAL
,
REAL
st ( for
x
being
real
number
holds
b
1
.
x
=
(
a
*
x
)
+
b
) & ( for
x
being
real
number
holds
b
2
.
x
=
(
a
*
x
)
+
b
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
AffineMap
FCONT_1:def 4 :
for
a
,
b
being
real
number
for
b
3
being
Function
of
REAL
,
REAL
holds
(
b
3
=
AffineMap
(
a
,
b
) iff for
x
being
real
number
holds
b
3
.
x
=
(
a
*
x
)
+
b
);
registration
let
a
,
b
be
real
number
;
cluster
AffineMap
(
a
,
b
)
->
continuous
;
coherence
AffineMap
(
a
,
b
) is
continuous
proof
end;
end;
registration
cluster
Relation-like
REAL
-defined
REAL
-valued
Function-like
non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
continuous
for
Element
of
bool
[:
REAL
,
REAL
:]
;
existence
ex
b
1
being
Function
of
REAL
,
REAL
st
b
1
is
continuous
proof
end;
end;
theorem
Th48
:
:: FCONT_1:48
for
a
,
b
being
real
number
holds
(
AffineMap
(
a
,
b
)
)
.
0
=
b
proof
end;
theorem
Th49
:
:: FCONT_1:49
for
a
,
b
being
real
number
holds
(
AffineMap
(
a
,
b
)
)
.
1
=
a
+
b
proof
end;
theorem
Th50
:
:: FCONT_1:50
for
a
,
b
being
real
number
st
a
<>
0
holds
AffineMap
(
a
,
b
) is
one-to-one
proof
end;
theorem
:: FCONT_1:51
for
a
,
b
,
x
,
y
being
real
number
st
a
>
0
&
x
<
y
holds
(
AffineMap
(
a
,
b
)
)
.
x
<
(
AffineMap
(
a
,
b
)
)
.
y
proof
end;
theorem
:: FCONT_1:52
for
a
,
b
,
x
,
y
being
real
number
st
a
<
0
&
x
<
y
holds
(
AffineMap
(
a
,
b
)
)
.
x
>
(
AffineMap
(
a
,
b
)
)
.
y
proof
end;
theorem
Th53
:
:: FCONT_1:53
for
a
,
b
,
x
,
y
being
real
number
st
a
>=
0
&
x
<=
y
holds
(
AffineMap
(
a
,
b
)
)
.
x
<=
(
AffineMap
(
a
,
b
)
)
.
y
proof
end;
theorem
:: FCONT_1:54
for
a
,
b
,
x
,
y
being
real
number
st
a
<=
0
&
x
<=
y
holds
(
AffineMap
(
a
,
b
)
)
.
x
>=
(
AffineMap
(
a
,
b
)
)
.
y
proof
end;
theorem
Th55
:
:: FCONT_1:55
for
a
,
b
being
real
number
st
a
<>
0
holds
rng
(
AffineMap
(
a
,
b
)
)
=
REAL
proof
end;
theorem
:: FCONT_1:56
for
a
,
b
being
real
number
st
a
<>
0
holds
(
AffineMap
(
a
,
b
)
)
"
=
AffineMap
(
(
a
"
)
,
(
-
(
b
/
a
)
)
)
proof
end;
theorem
:: FCONT_1:57
for
a
,
b
being
real
number
st
a
>
0
holds
(
AffineMap
(
a
,
b
)
)
.:
[.
0
,1
.]
=
[.
b
,
(
a
+
b
)
.]
proof
end;