:: The Continuous Functions on Normed Linear Spaces
:: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
theorem
:: NFCONT_1:1
for
S
being non
empty
addLoopStr
for
seq1
,
seq2
being
sequence
of
S
holds
seq1
-
seq2
=
seq1
+
(
-
seq2
)
proof
end;
theorem
Th2
:
:: NFCONT_1:2
for
S
being
RealNormSpace
for
seq
being
sequence
of
S
holds
-
seq
=
(
-
1
)
*
seq
proof
end;
definition
let
S
be
RealNormSpace
;
let
x0
be
Point
of
S
;
mode
Neighbourhood
of
x0
->
Subset
of
S
means
:
Def1
:
:: NFCONT_1:def 1
ex
g
being
Real
st
(
0
<
g
&
{
y
where
y
is
Point
of
S
:
||.
(
y
-
x0
)
.||
<
g
}
c=
it
);
existence
ex
b
1
being
Subset
of
S
ex
g
being
Real
st
(
0
<
g
&
{
y
where
y
is
Point
of
S
:
||.
(
y
-
x0
)
.||
<
g
}
c=
b
1
)
proof
end;
end;
::
deftheorem
Def1
defines
Neighbourhood
NFCONT_1:def 1 :
for
S
being
RealNormSpace
for
x0
being
Point
of
S
for
b
3
being
Subset
of
S
holds
(
b
3
is
Neighbourhood
of
x0
iff ex
g
being
Real
st
(
0
<
g
&
{
y
where
y
is
Point
of
S
:
||.
(
y
-
x0
)
.||
<
g
}
c=
b
3
) );
theorem
Th3
:
:: NFCONT_1:3
for
S
being
RealNormSpace
for
x0
being
Point
of
S
for
g
being
Real
st
0
<
g
holds
{
y
where
y
is
Point
of
S
:
||.
(
y
-
x0
)
.||
<
g
}
is
Neighbourhood
of
x0
proof
end;
theorem
Th4
:
:: NFCONT_1:4
for
S
being
RealNormSpace
for
x0
being
Point
of
S
for
N
being
Neighbourhood
of
x0
holds
x0
in
N
proof
end;
definition
let
S
be
RealNormSpace
;
let
X
be
Subset
of
S
;
attr
X
is
compact
means
:
Def2
:
:: NFCONT_1:def 2
for
s1
being
sequence
of
S
st
rng
s1
c=
X
holds
ex
s2
being
sequence
of
S
st
(
s2
is
subsequence
of
s1
&
s2
is
convergent
&
lim
s2
in
X
);
end;
::
deftheorem
Def2
defines
compact
NFCONT_1:def 2 :
for
S
being
RealNormSpace
for
X
being
Subset
of
S
holds
(
X
is
compact
iff for
s1
being
sequence
of
S
st
rng
s1
c=
X
holds
ex
s2
being
sequence
of
S
st
(
s2
is
subsequence
of
s1
&
s2
is
convergent
&
lim
s2
in
X
) );
definition
let
S
be
RealNormSpace
;
let
X
be
Subset
of
S
;
attr
X
is
closed
means
:: NFCONT_1:def 3
for
s1
being
sequence
of
S
st
rng
s1
c=
X
&
s1
is
convergent
holds
lim
s1
in
X
;
end;
::
deftheorem
defines
closed
NFCONT_1:def 3 :
for
S
being
RealNormSpace
for
X
being
Subset
of
S
holds
(
X
is
closed
iff for
s1
being
sequence
of
S
st
rng
s1
c=
X
&
s1
is
convergent
holds
lim
s1
in
X
);
definition
let
S
be
RealNormSpace
;
let
X
be
Subset
of
S
;
attr
X
is
open
means
:: NFCONT_1:def 4
X
`
is
closed
;
end;
::
deftheorem
defines
open
NFCONT_1:def 4 :
for
S
being
RealNormSpace
for
X
being
Subset
of
S
holds
(
X
is
open
iff
X
`
is
closed
);
definition
let
S
,
T
be
RealNormSpace
;
let
f
be
PartFunc
of
S
,
T
;
let
x0
be
Point
of
S
;
pred
f
is_continuous_in
x0
means
:
Def5
:
:: NFCONT_1:def 5
(
x0
in
dom
f
& ( for
s1
being
sequence
of
S
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
/.
x0
=
lim
(
f
/*
s1
)
) ) );
end;
::
deftheorem
Def5
defines
is_continuous_in
NFCONT_1:def 5 :
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
s1
being
sequence
of
S
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
/.
x0
=
lim
(
f
/*
s1
)
) ) ) );
definition
let
S
be
RealNormSpace
;
let
f
be
PartFunc
of the
carrier
of
S
,
REAL
;
let
x0
be
Point
of
S
;
pred
f
is_continuous_in
x0
means
:
Def6
:
:: NFCONT_1:def 6
(
x0
in
dom
f
& ( for
s1
being
sequence
of
S
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
/.
x0
=
lim
(
f
/*
s1
)
) ) );
end;
::
deftheorem
Def6
defines
is_continuous_in
NFCONT_1:def 6 :
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
for
x0
being
Point
of
S
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
s1
being
sequence
of
S
st
rng
s1
c=
dom
f
&
s1
is
convergent
&
lim
s1
=
x0
holds
(
f
/*
s1
is
convergent
&
f
/.
x0
=
lim
(
f
/*
s1
)
) ) ) );
theorem
Th5
:
:: NFCONT_1:5
for
n
being
Element
of
NAT
for
S
,
T
being
RealNormSpace
for
seq
being
sequence
of
S
for
h
being
PartFunc
of
S
,
T
st
rng
seq
c=
dom
h
holds
seq
.
n
in
dom
h
proof
end;
theorem
Th6
:
:: NFCONT_1:6
for
S
being
RealNormSpace
for
seq
being
sequence
of
S
for
x
being
set
holds
(
x
in
rng
seq
iff ex
n
being
Element
of
NAT
st
x
=
seq
.
n
)
proof
end;
theorem
Th7
:
:: NFCONT_1:7
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
r
being
Real
st
0
<
r
holds
ex
s
being
Real
st
(
0
<
s
& ( for
x1
being
Point
of
S
st
x1
in
dom
f
&
||.
(
x1
-
x0
)
.||
<
s
holds
||.
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
.||
<
r
) ) ) ) )
proof
end;
theorem
Th8
:
:: NFCONT_1:8
for
S
being
RealNormSpace
for
x0
being
Point
of
S
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
r
being
Real
st
0
<
r
holds
ex
s
being
Real
st
(
0
<
s
& ( for
x1
being
Point
of
S
st
x1
in
dom
f
&
||.
(
x1
-
x0
)
.||
<
s
holds
abs
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
<
r
) ) ) ) )
proof
end;
theorem
Th9
:
:: NFCONT_1:9
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
N1
being
Neighbourhood
of
f
/.
x0
ex
N
being
Neighbourhood
of
x0
st
for
x1
being
Point
of
S
st
x1
in
dom
f
&
x1
in
N
holds
f
/.
x1
in
N1
) ) )
proof
end;
theorem
Th10
:
:: NFCONT_1:10
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
holds
(
f
is_continuous_in
x0
iff (
x0
in
dom
f
& ( for
N1
being
Neighbourhood
of
f
/.
x0
ex
N
being
Neighbourhood
of
x0
st
f
.:
N
c=
N1
) ) )
proof
end;
theorem
:: NFCONT_1:11
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
st
x0
in
dom
f
& ex
N
being
Neighbourhood
of
x0
st
(
dom
f
)
/\
N
=
{
x0
}
holds
f
is_continuous_in
x0
proof
end;
theorem
Th12
:
:: NFCONT_1:12
for
S
,
T
being
RealNormSpace
for
h1
,
h2
being
PartFunc
of
S
,
T
for
seq
being
sequence
of
S
st
rng
seq
c=
(
dom
h1
)
/\
(
dom
h2
)
holds
(
(
h1
+
h2
)
/*
seq
=
(
h1
/*
seq
)
+
(
h2
/*
seq
)
&
(
h1
-
h2
)
/*
seq
=
(
h1
/*
seq
)
-
(
h2
/*
seq
)
)
proof
end;
theorem
Th13
:
:: NFCONT_1:13
for
S
,
T
being
RealNormSpace
for
h
being
PartFunc
of
S
,
T
for
seq
being
sequence
of
S
for
r
being
Real
st
rng
seq
c=
dom
h
holds
(
r
(#)
h
)
/*
seq
=
r
*
(
h
/*
seq
)
proof
end;
theorem
Th14
:
:: NFCONT_1:14
for
S
,
T
being
RealNormSpace
for
h
being
PartFunc
of
S
,
T
for
seq
being
sequence
of
S
st
rng
seq
c=
dom
h
holds
(
||.
(
h
/*
seq
)
.||
=
||.
h
.||
/*
seq
&
-
(
h
/*
seq
)
=
(
-
h
)
/*
seq
)
proof
end;
theorem
:: NFCONT_1:15
for
T
,
S
being
RealNormSpace
for
f1
,
f2
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
st
f1
is_continuous_in
x0
&
f2
is_continuous_in
x0
holds
(
f1
+
f2
is_continuous_in
x0
&
f1
-
f2
is_continuous_in
x0
)
proof
end;
theorem
Th16
:
:: NFCONT_1:16
for
r
being
Real
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
st
f
is_continuous_in
x0
holds
r
(#)
f
is_continuous_in
x0
proof
end;
theorem
:: NFCONT_1:17
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
st
f
is_continuous_in
x0
holds
(
||.
f
.||
is_continuous_in
x0
&
-
f
is_continuous_in
x0
)
proof
end;
definition
let
S
,
T
be
RealNormSpace
;
let
f
be
PartFunc
of
S
,
T
;
let
X
be
set
;
pred
f
is_continuous_on
X
means
:
Def7
:
:: NFCONT_1:def 7
(
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
|
X
is_continuous_in
x0
) );
end;
::
deftheorem
Def7
defines
is_continuous_on
NFCONT_1:def 7 :
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
X
being
set
holds
(
f
is_continuous_on
X
iff (
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
|
X
is_continuous_in
x0
) ) );
definition
let
S
be
RealNormSpace
;
let
f
be
PartFunc
of the
carrier
of
S
,
REAL
;
let
X
be
set
;
pred
f
is_continuous_on
X
means
:
Def8
:
:: NFCONT_1:def 8
(
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
|
X
is_continuous_in
x0
) );
end;
::
deftheorem
Def8
defines
is_continuous_on
NFCONT_1:def 8 :
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
for
X
being
set
holds
(
f
is_continuous_on
X
iff (
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
|
X
is_continuous_in
x0
) ) );
theorem
Th18
:
:: NFCONT_1:18
for
T
,
S
being
RealNormSpace
for
X
being
set
for
f
being
PartFunc
of
S
,
T
holds
(
f
is_continuous_on
X
iff (
X
c=
dom
f
& ( for
s1
being
sequence
of
S
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
Th19
:
:: NFCONT_1:19
for
X
being
set
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
holds
(
f
is_continuous_on
X
iff (
X
c=
dom
f
& ( for
x0
being
Point
of
S
for
r
being
Real
st
x0
in
X
&
0
<
r
holds
ex
s
being
Real
st
(
0
<
s
& ( for
x1
being
Point
of
S
st
x1
in
X
&
||.
(
x1
-
x0
)
.||
<
s
holds
||.
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
.||
<
r
) ) ) ) )
proof
end;
theorem
:: NFCONT_1:20
for
X
being
set
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
holds
(
f
is_continuous_on
X
iff (
X
c=
dom
f
& ( for
x0
being
Point
of
S
for
r
being
Real
st
x0
in
X
&
0
<
r
holds
ex
s
being
Real
st
(
0
<
s
& ( for
x1
being
Point
of
S
st
x1
in
X
&
||.
(
x1
-
x0
)
.||
<
s
holds
abs
(
(
f
/.
x1
)
-
(
f
/.
x0
)
)
<
r
) ) ) ) )
proof
end;
theorem
:: NFCONT_1:21
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
holds
(
f
is_continuous_on
X
iff
f
|
X
is_continuous_on
X
)
proof
end;
theorem
Th22
:
:: NFCONT_1:22
for
X
being
set
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
holds
(
f
is_continuous_on
X
iff
f
|
X
is_continuous_on
X
)
proof
end;
theorem
Th23
:
:: NFCONT_1:23
for
X
,
X1
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_continuous_on
X
&
X1
c=
X
holds
f
is_continuous_on
X1
proof
end;
theorem
:: NFCONT_1:24
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
x0
being
Point
of
S
st
x0
in
dom
f
holds
f
is_continuous_on
{
x0
}
proof
end;
theorem
Th25
:
:: NFCONT_1:25
for
T
,
S
being
RealNormSpace
for
X
being
set
for
f1
,
f2
being
PartFunc
of
S
,
T
st
f1
is_continuous_on
X
&
f2
is_continuous_on
X
holds
(
f1
+
f2
is_continuous_on
X
&
f1
-
f2
is_continuous_on
X
)
proof
end;
theorem
:: NFCONT_1:26
for
T
,
S
being
RealNormSpace
for
X
,
X1
being
set
for
f1
,
f2
being
PartFunc
of
S
,
T
st
f1
is_continuous_on
X
&
f2
is_continuous_on
X1
holds
(
f1
+
f2
is_continuous_on
X
/\
X1
&
f1
-
f2
is_continuous_on
X
/\
X1
)
proof
end;
theorem
Th27
:
:: NFCONT_1:27
for
T
,
S
being
RealNormSpace
for
r
being
Real
for
X
being
set
for
f
being
PartFunc
of
S
,
T
st
f
is_continuous_on
X
holds
r
(#)
f
is_continuous_on
X
proof
end;
theorem
Th28
:
:: NFCONT_1:28
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_continuous_on
X
holds
(
||.
f
.||
is_continuous_on
X
&
-
f
is_continuous_on
X
)
proof
end;
theorem
:: NFCONT_1:29
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is
total
& ( for
x1
,
x2
being
Point
of
S
holds
f
/.
(
x1
+
x2
)
=
(
f
/.
x1
)
+
(
f
/.
x2
)
) & ex
x0
being
Point
of
S
st
f
is_continuous_in
x0
holds
f
is_continuous_on
the
carrier
of
S
proof
end;
theorem
Th30
:
:: NFCONT_1:30
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
dom
f
is
compact
&
f
is_continuous_on
dom
f
holds
rng
f
is
compact
proof
end;
theorem
Th31
:
:: NFCONT_1:31
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
st
dom
f
is
compact
&
f
is_continuous_on
dom
f
holds
rng
f
is
compact
proof
end;
theorem
:: NFCONT_1:32
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
Y
being
Subset
of
S
st
Y
c=
dom
f
&
Y
is
compact
&
f
is_continuous_on
Y
holds
f
.:
Y
is
compact
proof
end;
theorem
Th33
:
:: NFCONT_1:33
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
st
dom
f
<>
{}
&
dom
f
is
compact
&
f
is_continuous_on
dom
f
holds
ex
x1
,
x2
being
Point
of
S
st
(
x1
in
dom
f
&
x2
in
dom
f
&
f
/.
x1
=
upper_bound
(
rng
f
)
&
f
/.
x2
=
lower_bound
(
rng
f
)
)
proof
end;
theorem
Th34
:
:: NFCONT_1:34
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
dom
f
<>
{}
&
dom
f
is
compact
&
f
is_continuous_on
dom
f
holds
ex
x1
,
x2
being
Point
of
S
st
(
x1
in
dom
f
&
x2
in
dom
f
&
||.
f
.||
/.
x1
=
upper_bound
(
rng
||.
f
.||
)
&
||.
f
.||
/.
x2
=
lower_bound
(
rng
||.
f
.||
)
)
proof
end;
theorem
Th35
:
:: NFCONT_1:35
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
holds
||.
f
.||
|
X
=
||.
(
f
|
X
)
.||
proof
end;
theorem
:: NFCONT_1:36
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
for
Y
being
Subset
of
S
st
Y
<>
{}
&
Y
c=
dom
f
&
Y
is
compact
&
f
is_continuous_on
Y
holds
ex
x1
,
x2
being
Point
of
S
st
(
x1
in
Y
&
x2
in
Y
&
||.
f
.||
/.
x1
=
upper_bound
(
||.
f
.||
.:
Y
)
&
||.
f
.||
/.
x2
=
lower_bound
(
||.
f
.||
.:
Y
)
)
proof
end;
theorem
:: NFCONT_1:37
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
for
Y
being
Subset
of
S
st
Y
<>
{}
&
Y
c=
dom
f
&
Y
is
compact
&
f
is_continuous_on
Y
holds
ex
x1
,
x2
being
Point
of
S
st
(
x1
in
Y
&
x2
in
Y
&
f
/.
x1
=
upper_bound
(
f
.:
Y
)
&
f
/.
x2
=
lower_bound
(
f
.:
Y
)
)
proof
end;
definition
let
S
,
T
be
RealNormSpace
;
let
X
be
set
;
let
f
be
PartFunc
of
S
,
T
;
pred
f
is_Lipschitzian_on
X
means
:
Def9
:
:: NFCONT_1:def 9
(
X
c=
dom
f
& ex
r
being
Real
st
(
0
<
r
& ( for
x1
,
x2
being
Point
of
S
st
x1
in
X
&
x2
in
X
holds
||.
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
.||
<=
r
*
||.
(
x1
-
x2
)
.||
) ) );
end;
::
deftheorem
Def9
defines
is_Lipschitzian_on
NFCONT_1:def 9 :
for
S
,
T
being
RealNormSpace
for
X
being
set
for
f
being
PartFunc
of
S
,
T
holds
(
f
is_Lipschitzian_on
X
iff (
X
c=
dom
f
& ex
r
being
Real
st
(
0
<
r
& ( for
x1
,
x2
being
Point
of
S
st
x1
in
X
&
x2
in
X
holds
||.
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
.||
<=
r
*
||.
(
x1
-
x2
)
.||
) ) ) );
definition
let
S
be
RealNormSpace
;
let
X
be
set
;
let
f
be
PartFunc
of the
carrier
of
S
,
REAL
;
pred
f
is_Lipschitzian_on
X
means
:
Def10
:
:: NFCONT_1:def 10
(
X
c=
dom
f
& ex
r
being
Real
st
(
0
<
r
& ( for
x1
,
x2
being
Point
of
S
st
x1
in
X
&
x2
in
X
holds
abs
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
<=
r
*
||.
(
x1
-
x2
)
.||
) ) );
end;
::
deftheorem
Def10
defines
is_Lipschitzian_on
NFCONT_1:def 10 :
for
S
being
RealNormSpace
for
X
being
set
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
holds
(
f
is_Lipschitzian_on
X
iff (
X
c=
dom
f
& ex
r
being
Real
st
(
0
<
r
& ( for
x1
,
x2
being
Point
of
S
st
x1
in
X
&
x2
in
X
holds
abs
(
(
f
/.
x1
)
-
(
f
/.
x2
)
)
<=
r
*
||.
(
x1
-
x2
)
.||
) ) ) );
theorem
Th38
:
:: NFCONT_1:38
for
X
,
X1
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_Lipschitzian_on
X
&
X1
c=
X
holds
f
is_Lipschitzian_on
X1
proof
end;
theorem
:: NFCONT_1:39
for
X
,
X1
being
set
for
S
,
T
being
RealNormSpace
for
f1
,
f2
being
PartFunc
of
S
,
T
st
f1
is_Lipschitzian_on
X
&
f2
is_Lipschitzian_on
X1
holds
f1
+
f2
is_Lipschitzian_on
X
/\
X1
proof
end;
theorem
:: NFCONT_1:40
for
X
,
X1
being
set
for
S
,
T
being
RealNormSpace
for
f1
,
f2
being
PartFunc
of
S
,
T
st
f1
is_Lipschitzian_on
X
&
f2
is_Lipschitzian_on
X1
holds
f1
-
f2
is_Lipschitzian_on
X
/\
X1
proof
end;
theorem
Th41
:
:: NFCONT_1:41
for
X
being
set
for
p
being
Real
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_Lipschitzian_on
X
holds
p
(#)
f
is_Lipschitzian_on
X
proof
end;
theorem
:: NFCONT_1:42
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_Lipschitzian_on
X
holds
(
-
f
is_Lipschitzian_on
X
&
||.
f
.||
is_Lipschitzian_on
X
)
proof
end;
theorem
Th43
:
:: NFCONT_1:43
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
X
c=
dom
f
&
f
|
X
is
V23
() holds
f
is_Lipschitzian_on
X
proof
end;
theorem
:: NFCONT_1:44
for
S
being
RealNormSpace
for
Y
being
Subset
of
S
holds
id
Y
is_Lipschitzian_on
Y
proof
end;
theorem
Th45
:
:: NFCONT_1:45
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
f
is_Lipschitzian_on
X
holds
f
is_continuous_on
X
proof
end;
theorem
Th46
:
:: NFCONT_1:46
for
X
being
set
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
st
f
is_Lipschitzian_on
X
holds
f
is_continuous_on
X
proof
end;
theorem
:: NFCONT_1:47
for
T
,
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st ex
r
being
Point
of
T
st
rng
f
=
{
r
}
holds
f
is_continuous_on
dom
f
proof
end;
theorem
:: NFCONT_1:48
for
X
being
set
for
S
,
T
being
RealNormSpace
for
f
being
PartFunc
of
S
,
T
st
X
c=
dom
f
&
f
|
X
is
V23
() holds
f
is_continuous_on
X
by
Th43
,
Th45
;
theorem
Th49
:
:: NFCONT_1:49
for
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
S
st ( for
x0
being
Point
of
S
st
x0
in
dom
f
holds
f
/.
x0
=
x0
) holds
f
is_continuous_on
dom
f
proof
end;
theorem
:: NFCONT_1:50
for
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
S
st
f
=
id
(
dom
f
)
holds
f
is_continuous_on
dom
f
proof
end;
theorem
:: NFCONT_1:51
for
S
being
RealNormSpace
for
Y
being
Subset
of
S
for
f
being
PartFunc
of
S
,
S
st
Y
c=
dom
f
&
f
|
Y
=
id
Y
holds
f
is_continuous_on
Y
proof
end;
theorem
:: NFCONT_1:52
for
X
being
set
for
S
being
RealNormSpace
for
f
being
PartFunc
of
S
,
S
for
r
being
Real
for
p
being
Point
of
S
st
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
/.
x0
=
(
r
*
x0
)
+
p
) holds
f
is_continuous_on
X
proof
end;
theorem
Th53
:
:: NFCONT_1:53
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
st ( for
x0
being
Point
of
S
st
x0
in
dom
f
holds
f
/.
x0
=
||.
x0
.||
) holds
f
is_continuous_on
dom
f
proof
end;
theorem
:: NFCONT_1:54
for
X
being
set
for
S
being
RealNormSpace
for
f
being
PartFunc
of the
carrier
of
S
,
REAL
st
X
c=
dom
f
& ( for
x0
being
Point
of
S
st
x0
in
X
holds
f
/.
x0
=
||.
x0
.||
) holds
f
is_continuous_on
X
proof
end;