:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users
begin
definition
let
n
be
Element
of
NAT
;
let
f
be
PartFunc
of
REAL
,
(
REAL
n
)
;
let
x0
be
real
number
;
pred
f
is_continuous_in
x0
means
:
Def1
:
:: NFCONT_4:def 1
ex
g
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
(
f
=
g
&
g
is_continuous_in
x0
);
end;
::
deftheorem
Def1
defines
is_continuous_in
NFCONT_4:def 1 :
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
x0
being
real
number
holds
(
f
is_continuous_in
x0
iff ex
g
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
(
f
=
g
&
g
is_continuous_in
x0
) );
theorem
Th1
:
:: NFCONT_4:1
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
h
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
h
=
f
holds
(
f
is_continuous_in
x0
iff
h
is_continuous_in
x0
)
proof
end;
theorem
Th2
:
:: NFCONT_4:2
for
n
being
Element
of
NAT
for
X
being
set
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
x0
in
X
&
f
is_continuous_in
x0
holds
f
|
X
is_continuous_in
x0
proof
end;
theorem
Th3
:
:: NFCONT_4:3
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
r
being
Real
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
|.
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
.|
<
r
) ) ) ) )
proof
end;
theorem
Th4
:
:: NFCONT_4:4
for
n
being
Element
of
NAT
for
r
being
Real
for
z
being
Element
of
REAL
n
for
w
being
Point
of
(
REAL-NS
n
)
st
z
=
w
holds
{
y
where
y
is
Element
of
REAL
n
:
|.
(
y
-
z
)
.|
<
r
}
=
{
y
where
y
is
Point
of
(
REAL-NS
n
)
:
||.
(
y
-
w
)
.||
<
r
}
proof
end;
definition
let
n
be
Element
of
NAT
;
let
Z
be
set
;
let
f
be
PartFunc
of
Z
,
(
REAL
n
)
;
deffunc
H
1
(
set
)
->
Element
of
REAL
=
|.
(
f
/.
$1
)
.|
;
func
|.
f
.|
->
PartFunc
of
Z
,
REAL
means
:
Def2
:
:: NFCONT_4:def 2
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
/.
x
=
|.
(
f
/.
x
)
.|
) );
existence
ex
b
1
being
PartFunc
of
Z
,
REAL
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
/.
x
=
|.
(
f
/.
x
)
.|
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
Z
,
REAL
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
/.
x
=
|.
(
f
/.
x
)
.|
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
/.
x
=
|.
(
f
/.
x
)
.|
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
|.
NFCONT_4:def 2 :
for
n
being
Element
of
NAT
for
Z
being
set
for
f
being
PartFunc
of
Z
,
(
REAL
n
)
for
b
4
being
PartFunc
of
Z
,
REAL
holds
(
b
4
=
|.
f
.|
iff (
dom
b
4
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
4
holds
b
4
/.
x
=
|.
(
f
/.
x
)
.|
) ) );
definition
let
n
be
Element
of
NAT
;
let
Z
be non
empty
set
;
let
f
be
PartFunc
of
Z
,
(
REAL
n
)
;
deffunc
H
1
(
set
)
->
M13
(
REAL
,
REAL
n
) =
-
(
f
/.
$1
)
;
defpred
S
1
[
set
]
means
$1
in
dom
f
;
func
-
f
->
PartFunc
of
Z
,
(
REAL
n
)
means
:
Def3
:
:: NFCONT_4:def 3
(
dom
it
=
dom
f
& ( for
c
being
set
st
c
in
dom
it
holds
it
/.
c
=
-
(
f
/.
c
)
) );
existence
ex
b
1
being
PartFunc
of
Z
,
(
REAL
n
)
st
(
dom
b
1
=
dom
f
& ( for
c
being
set
st
c
in
dom
b
1
holds
b
1
/.
c
=
-
(
f
/.
c
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
Z
,
(
REAL
n
)
st
dom
b
1
=
dom
f
& ( for
c
being
set
st
c
in
dom
b
1
holds
b
1
/.
c
=
-
(
f
/.
c
)
) &
dom
b
2
=
dom
f
& ( for
c
being
set
st
c
in
dom
b
2
holds
b
2
/.
c
=
-
(
f
/.
c
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
-
NFCONT_4:def 3 :
for
n
being
Element
of
NAT
for
Z
being non
empty
set
for
f
,
b
4
being
PartFunc
of
Z
,
(
REAL
n
)
holds
(
b
4
=
-
f
iff (
dom
b
4
=
dom
f
& ( for
c
being
set
st
c
in
dom
b
4
holds
b
4
/.
c
=
-
(
f
/.
c
)
) ) );
theorem
Th5
:
:: NFCONT_4:5
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
,
f2
being
PartFunc
of
W
,
(
REAL-NS
n
)
for
g1
,
g2
being
PartFunc
of
W
,
(
REAL
n
)
st
f1
=
g1
&
f2
=
g2
holds
f1
+
f2
=
g1
+
g2
proof
end;
theorem
Th6
:
:: NFCONT_4:6
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
being
PartFunc
of
W
,
(
REAL-NS
n
)
for
g1
being
PartFunc
of
W
,
(
REAL
n
)
for
a
being
Real
st
f1
=
g1
holds
a
(#)
f1
=
a
(#)
g1
proof
end;
theorem
:: NFCONT_4:7
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
being
PartFunc
of
W
,
(
REAL
n
)
holds
(
-
1
)
(#)
f1
=
-
f1
proof
end;
theorem
Th8
:
:: NFCONT_4:8
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
being
PartFunc
of
W
,
(
REAL-NS
n
)
for
g1
being
PartFunc
of
W
,
(
REAL
n
)
st
f1
=
g1
holds
-
f1
=
-
g1
proof
end;
theorem
Th9
:
:: NFCONT_4:9
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
being
PartFunc
of
W
,
(
REAL-NS
n
)
for
g1
being
PartFunc
of
W
,
(
REAL
n
)
st
f1
=
g1
holds
||.
f1
.||
=
|.
g1
.|
proof
end;
theorem
Th10
:
:: NFCONT_4:10
for
n
being
Element
of
NAT
for
W
being non
empty
set
for
f1
,
f2
being
PartFunc
of
W
,
(
REAL-NS
n
)
for
g1
,
g2
being
PartFunc
of
W
,
(
REAL
n
)
st
f1
=
g1
&
f2
=
g2
holds
f1
-
f2
=
g1
-
g2
proof
end;
theorem
:: NFCONT_4:11
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
N1
being
Subset
of
(
REAL
n
)
st ex
r
being
Real
st
(
0
<
r
&
{
y
where
y
is
Element
of
REAL
n
:
|.
(
y
-
(
f
/.
x0
)
)
.|
<
r
}
=
N1
) holds
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
:: NFCONT_4:12
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
N1
being
Subset
of
(
REAL
n
)
st ex
r
being
Real
st
(
0
<
r
&
{
y
where
y
is
Element
of
REAL
n
:
|.
(
y
-
(
f
/.
x0
)
)
.|
<
r
}
=
N1
) holds
ex
N
being
Neighbourhood
of
x0
st
f
.:
N
c=
N1
) ) )
proof
end;
theorem
:: NFCONT_4:13
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st ex
N
being
Neighbourhood
of
x0
st
(
dom
f
)
/\
N
=
{
x0
}
holds
f
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:14
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
st
x0
in
(
dom
f1
)
/\
(
dom
f2
)
&
f1
is_continuous_in
x0
&
f2
is_continuous_in
x0
holds
f1
+
f2
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:15
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
st
x0
in
(
dom
f1
)
/\
(
dom
f2
)
&
f1
is_continuous_in
x0
&
f2
is_continuous_in
x0
holds
f1
-
f2
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:16
for
n
being
Element
of
NAT
for
r
being
Real
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f
is_continuous_in
x0
holds
r
(#)
f
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:17
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
x0
in
dom
f
&
f
is_continuous_in
x0
holds
|.
f
.|
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:18
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
x0
in
dom
f
&
f
is_continuous_in
x0
holds
-
f
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_4:19
for
n
being
Element
of
NAT
for
x0
being
real
number
for
S
being
RealNormSpace
for
z
being
Point
of
(
REAL-NS
n
)
for
f1
being
PartFunc
of
REAL
,
(
REAL
n
)
for
f2
being
PartFunc
of
(
REAL-NS
n
)
,
S
st
x0
in
dom
(
f2
*
f1
)
&
f1
is_continuous_in
x0
&
z
=
f1
/.
x0
&
f2
is_continuous_in
z
holds
f2
*
f1
is_continuous_in
x0
proof
end;
theorem
Th20
:
:: NFCONT_4:20
for
x0
being
real
number
for
S
being
RealNormSpace
for
f1
being
PartFunc
of
REAL
,
S
for
f2
being
PartFunc
of
S
,
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
n
be
Element
of
NAT
;
let
f
be
PartFunc
of
(
REAL
n
)
,
REAL
;
let
x0
be
Element
of
REAL
n
;
pred
f
is_continuous_in
x0
means
:
Def4
:
:: NFCONT_4:def 4
ex
y0
being
Point
of
(
REAL-NS
n
)
ex
g
being
PartFunc
of
(
REAL-NS
n
)
,
REAL
st
(
x0
=
y0
&
f
=
g
&
g
is_continuous_in
y0
);
end;
::
deftheorem
Def4
defines
is_continuous_in
NFCONT_4:def 4 :
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
(
REAL
n
)
,
REAL
for
x0
being
Element
of
REAL
n
holds
(
f
is_continuous_in
x0
iff ex
y0
being
Point
of
(
REAL-NS
n
)
ex
g
being
PartFunc
of
(
REAL-NS
n
)
,
REAL
st
(
x0
=
y0
&
f
=
g
&
g
is_continuous_in
y0
) );
theorem
Th21
:
:: NFCONT_4:21
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
(
REAL
n
)
,
REAL
for
h
being
PartFunc
of
(
REAL-NS
n
)
,
REAL
for
x0
being
Element
of
REAL
n
for
y0
being
Point
of
(
REAL-NS
n
)
st
f
=
h
&
x0
=
y0
holds
(
f
is_continuous_in
x0
iff
h
is_continuous_in
y0
)
proof
end;
theorem
Th22
:
:: NFCONT_4:22
for
n
being
Element
of
NAT
for
x0
being
real
number
for
f1
being
PartFunc
of
REAL
,
(
REAL
n
)
for
f2
being
PartFunc
of
(
REAL
n
)
,
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
n
be
Element
of
NAT
;
let
f
be
PartFunc
of
REAL
,
(
REAL
n
)
;
attr
f
is
continuous
means
:
Def5
:
:: NFCONT_4:def 5
for
x0
being
real
number
st
x0
in
dom
f
holds
f
is_continuous_in
x0
;
end;
::
deftheorem
Def5
defines
continuous
NFCONT_4:def 5 :
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is
continuous
iff for
x0
being
real
number
st
x0
in
dom
f
holds
f
is_continuous_in
x0
);
theorem
Th23
:
:: NFCONT_4:23
for
n
being
Element
of
NAT
for
g
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
g
=
f
holds
(
g
is
continuous
iff
f
is
continuous
)
proof
end;
theorem
Th24
:
:: NFCONT_4:24
for
n
being
Element
of
NAT
for
X
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
X
c=
dom
f
holds
(
f
|
X
is
continuous
iff for
x0
being
real
number
for
r
being
Real
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
|.
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
.|
<
r
) ) )
proof
end;
registration
let
n
be
Element
of
NAT
;
cluster
Function-like
constant
->
continuous
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
constant
holds
b
1
is
continuous
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
cluster
Relation-like
REAL
-defined
REAL
n
-valued
Function-like
V233
()
V234
()
V235
()
continuous
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
existence
ex
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
continuous
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
continuous
PartFunc
of
REAL
,
(
REAL
n
)
;
let
X
be
set
;
cluster
f
|
X
->
continuous
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f
|
X
holds
b
1
is
continuous
proof
end;
end;
theorem
:: NFCONT_4:25
for
n
being
Element
of
NAT
for
X
,
X1
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f
|
X
is
continuous
&
X1
c=
X
holds
f
|
X1
is
continuous
proof
end;
registration
let
n
be
Element
of
NAT
;
cluster
empty
Function-like
->
continuous
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
empty
holds
b
1
is
continuous
;
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
PartFunc
of
REAL
,
(
REAL
n
)
;
let
X
be
trivial
set
;
cluster
f
|
X
->
continuous
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f
|
X
holds
b
1
is
continuous
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
let
f1
,
f2
be
continuous
PartFunc
of
REAL
,
(
REAL
n
)
;
cluster
f1
+
f2
->
continuous
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f1
+
f2
holds
b
1
is
continuous
proof
end;
end;
theorem
:: NFCONT_4:26
for
n
being
Element
of
NAT
for
X
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
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
)
proof
end;
theorem
:: NFCONT_4:27
for
n
being
Element
of
NAT
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
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
)
proof
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
continuous
PartFunc
of
REAL
,
(
REAL
n
)
;
let
r
be
Real
;
cluster
r
(#)
f
->
continuous
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
r
(#)
f
holds
b
1
is
continuous
proof
end;
end;
theorem
:: NFCONT_4:28
for
n
being
Element
of
NAT
for
X
being
set
for
r
being
Real
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
X
c=
dom
f
&
f
|
X
is
continuous
holds
(
r
(#)
f
)
|
X
is
continuous
proof
end;
theorem
:: NFCONT_4:29
for
n
being
Element
of
NAT
for
X
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
X
c=
dom
f
&
f
|
X
is
continuous
holds
(
|.
f
.|
|
X
is
continuous
&
(
-
f
)
|
X
is
continuous
)
proof
end;
theorem
:: NFCONT_4:30
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
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
:: NFCONT_4:31
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
Y
being
Subset
of
(
REAL-NS
n
)
st
dom
f
is
compact
&
f
|
(
dom
f
)
is
continuous
&
Y
=
rng
f
holds
Y
is
compact
proof
end;
theorem
:: NFCONT_4:32
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
Y
being
Subset
of
REAL
for
Z
being
Subset
of
(
REAL-NS
n
)
st
Y
c=
dom
f
&
Z
=
f
.:
Y
&
Y
is
compact
&
f
|
Y
is
continuous
holds
Z
is
compact
proof
end;
definition
let
n
be
Element
of
NAT
;
let
f
be
PartFunc
of
REAL
,
(
REAL
n
)
;
attr
f
is
Lipschitzian
means
:
Def6
:
:: NFCONT_4:def 6
ex
g
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
(
g
=
f
&
g
is
Lipschitzian
);
end;
::
deftheorem
Def6
defines
Lipschitzian
NFCONT_4:def 6 :
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is
Lipschitzian
iff ex
g
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
(
g
=
f
&
g
is
Lipschitzian
) );
theorem
Th33
:
:: NFCONT_4:33
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
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
|.
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
.|
<=
r
*
(
abs
(
x1
-
x2
)
)
) ) )
proof
end;
theorem
Th34
:
:: NFCONT_4:34
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
h
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
st
f
=
h
holds
(
f
is
Lipschitzian
iff
h
is
Lipschitzian
)
proof
end;
theorem
:: NFCONT_4:35
for
n
being
Element
of
NAT
for
X
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
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
|.
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
.|
<=
r
*
(
abs
(
x1
-
x2
)
)
) ) )
proof
end;
registration
let
n
be
Element
of
NAT
;
cluster
empty
Function-like
->
Lipschitzian
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
empty
holds
b
1
is
Lipschitzian
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
cluster
empty
Relation-like
REAL
-defined
REAL
n
-valued
Function-like
V233
()
V234
()
V235
() for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
existence
ex
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
empty
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
Lipschitzian
PartFunc
of
REAL
,
(
REAL
n
)
;
let
X
be
set
;
cluster
f
|
X
->
Lipschitzian
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f
|
X
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: NFCONT_4:36
for
n
being
Element
of
NAT
for
X
,
X1
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f
|
X
is
Lipschitzian
&
X1
c=
X
holds
f
|
X1
is
Lipschitzian
proof
end;
registration
let
n
be
Element
of
NAT
;
let
f1
,
f2
be
Lipschitzian
PartFunc
of
REAL
,
(
REAL
n
)
;
cluster
f1
+
f2
->
Lipschitzian
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f1
+
f2
holds
b
1
is
Lipschitzian
proof
end;
cluster
f1
-
f2
->
Lipschitzian
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
f1
-
f2
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: NFCONT_4:37
for
n
being
Element
of
NAT
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f1
|
X
is
Lipschitzian
&
f2
|
X1
is
Lipschitzian
holds
(
f1
+
f2
)
|
(
X
/\
X1
)
is
Lipschitzian
proof
end;
theorem
:: NFCONT_4:38
for
n
being
Element
of
NAT
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f1
|
X
is
Lipschitzian
&
f2
|
X1
is
Lipschitzian
holds
(
f1
-
f2
)
|
(
X
/\
X1
)
is
Lipschitzian
proof
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
Lipschitzian
PartFunc
of
REAL
,
(
REAL
n
)
;
let
p
be
Real
;
cluster
p
(#)
f
->
Lipschitzian
for
PartFunc
of
REAL
,
(
REAL
n
)
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
=
p
(#)
f
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: NFCONT_4:39
for
n
being
Element
of
NAT
for
X
being
set
for
p
being
Real
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f
|
X
is
Lipschitzian
&
X
c=
dom
f
holds
(
p
(#)
f
)
|
X
is
Lipschitzian
proof
end;
registration
let
n
be
Element
of
NAT
;
let
f
be
Lipschitzian
PartFunc
of
REAL
,
(
REAL
n
)
;
cluster
|.
f
.|
->
Lipschitzian
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
|.
f
.|
holds
b
1
is
Lipschitzian
proof
end;
end;
theorem
:: NFCONT_4:40
for
n
being
Element
of
NAT
for
X
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
f
|
X
is
Lipschitzian
holds
(
-
(
f
|
X
)
is
Lipschitzian
&
|.
f
.|
|
X
is
Lipschitzian
&
(
-
f
)
|
X
is
Lipschitzian
)
proof
end;
registration
let
n
be
Element
of
NAT
;
cluster
Function-like
constant
->
Lipschitzian
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
constant
holds
b
1
is
Lipschitzian
proof
end;
end;
registration
let
n
be
Element
of
NAT
;
cluster
Function-like
Lipschitzian
->
continuous
for
Element
of
bool
[:
REAL
,
(
REAL
n
)
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
(
REAL
n
)
st
b
1
is
Lipschitzian
holds
b
1
is
continuous
proof
end;
end;
theorem
:: NFCONT_4:41
for
n
being
Element
of
NAT
for
X
being
set
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
r
,
p
being
Element
of
REAL
n
st ( for
x0
being
real
number
st
x0
in
X
holds
f
/.
x0
=
(
x0
*
r
)
+
p
) holds
f
|
X
is
continuous
proof
end;
theorem
Th42
:
:: NFCONT_4:42
for
n
,
i
being
Element
of
NAT
for
x0
being
Element
of
REAL
n
st 1
<=
i
&
i
<=
n
holds
proj
(
i
,
n
)
is_continuous_in
x0
proof
end;
theorem
Th43
:
:: NFCONT_4:43
for
x0
being
real
number
for
n
being non
empty
Element
of
NAT
for
h
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
h
is_continuous_in
x0
iff (
x0
in
dom
h
& ( for
i
being
Element
of
NAT
st
i
in
Seg
n
holds
(
proj
(
i
,
n
)
)
*
h
is_continuous_in
x0
) ) )
proof
end;
theorem
:: NFCONT_4:44
for
n
being non
empty
Element
of
NAT
for
h
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
h
is
continuous
iff for
i
being
Element
of
NAT
st
i
in
Seg
n
holds
(
proj
(
i
,
n
)
)
*
h
is
continuous
)
proof
end;
theorem
Th45
:
:: NFCONT_4:45
for
n
,
i
being
Element
of
NAT
for
x0
being
Point
of
(
REAL-NS
n
)
st 1
<=
i
&
i
<=
n
holds
Proj
(
i
,
n
)
is_continuous_in
x0
proof
end;
theorem
Th46
:
:: NFCONT_4:46
for
x0
being
real
number
for
n
being non
empty
Element
of
NAT
for
h
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
holds
(
h
is_continuous_in
x0
iff for
i
being
Element
of
NAT
st
i
in
Seg
n
holds
(
Proj
(
i
,
n
)
)
*
h
is_continuous_in
x0
)
proof
end;
theorem
:: NFCONT_4:47
for
n
being non
empty
Element
of
NAT
for
h
being
PartFunc
of
REAL
,
(
REAL-NS
n
)
holds
(
h
is
continuous
iff for
i
being
Element
of
NAT
st
i
in
Seg
n
holds
(
Proj
(
i
,
n
)
)
*
h
is
continuous
)
proof
end;